let AS be AffinSpace; :: thesis: for A, C being Subset of AS st A // C holds
( A is being_line & C is being_line )
let A, C be Subset of AS; :: thesis: ( A // C implies ( A is being_line & C is being_line ) )
assume A // C ; :: thesis: ( A is being_line & C is being_line )
then ex a, b being Element of AS st
( A = Line (a,b) & a <> b & a,b // C ) ;
hence ( A is being_line & C is being_line ) ; :: thesis: verum