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 )

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

( 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

given a, b, c, d being Element of AS such that A4:
a <> b
and
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;( 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

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