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

( 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