A Suslin tree yields a Suslin line

Apply F2 to $T$ and obtain an infinitely splitting normal Suslin refinement $S$.

By F3, the maximal branches of $S$, ordered at their first differing successor, form a nonempty dense linear order $L$ without endpoints. The order has no uncountable pairwise disjoint family of nonempty open intervals, and every nonempty open interval of $L$ is nonseparable.

Take the exact completion of $L$ and delete its possible first and last points. By F4 the resulting order $M$ is nonempty, dense, has no endpoints, is boundedly complete, satisfies the interval ccc, and has no separable nonempty open interval. In particular $M$ itself has no countable order-dense subset: if such a set existed, it would be dense in every nonempty open subinterval, contradicting the preceding property. Thus every clause of F1 holds, so $M$ is a Suslin line in the published convention. All three constructions are in ZFC and their uses of choice are exactly those recorded by the supplying lemmas; the implication is not asserted in ZF.