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
A7: A = Line (a,b) and
A8: a <> b and
A9: a,b // C by Def5;
ex c, d being Element of AS st
( c <> d & C = Line (c,d) & a,b // c,d ) by A9, Def4;
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 A7, A8; :: thesis: verum

end;

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