let AS be AffinSpace; :: thesis: for A, C being Subset of AS holds
( A // C iff ex a, b, c, d being Element of AS st
( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) ) )
let A, C be Subset of AS; :: thesis: ( A // C iff ex a, b, c, d being Element of AS st
( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) ) )
thus ( A // C implies ex a, b, c, d being Element of AS st
( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) ) ) :: thesis: ( ex a, b, c, d being Element of AS st
( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) ) implies A // C )

proof

assume A // C ; :: thesis: ex a, b, c, d being Element of AS st
( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) )
then consider a, b being Element of AS such that
A1: A = Line (a,b) and
A2: a <> b and
A3: a,b // C ;
ex c, d being Element of AS st
( c <> d & C = Line (c,d) & a,b // c,d ) by A3;
hence ex a, b, c, d being Element of AS st
( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) ) by A1, A2; :: thesis: verum

end;

given a, b, c, d being Element of AS such that A4: a <> b and
A5: c <> d and
A6: a,b // c,d and
A7: A = Line (a,b) and
A8: C = Line (c,d) ; :: thesis: A // C
a,b // C by A5, A6, A8;
hence A // C by A4, A7; :: thesis: verum