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 ) )
A1: ( 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 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: A // C
then consider 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 ;
a,b // C by A3, A4, A6, Def4;
hence A // C by A2, A5, Def5; :: thesis: verum

end;

( 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 ) )

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;

hence ( 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 ) ) by A1; :: thesis: verum