let AS be AffinSpace; :: thesis: for a, b, c, d being Element of AS
for X, Y, Z being Subset of AS st X is being_plane & Y is being_plane & Z is being_plane & X '||' Y & X <> Y & a in X /\ Z & b in X /\ Z & c in Y /\ Z & d in Y /\ Z holds
a,b // c,d
let a, b, c, d be Element of AS; :: thesis: for X, Y, Z being Subset of AS st X is being_plane & Y is being_plane & Z is being_plane & X '||' Y & X <> Y & a in X /\ Z & b in X /\ Z & c in Y /\ Z & d in Y /\ Z holds
a,b // c,d
let X, Y, Z be Subset of AS; :: thesis: ( X is being_plane & Y is being_plane & Z is being_plane & X '||' Y & X <> Y & a in X /\ Z & b in X /\ Z & c in Y /\ Z & d in Y /\ Z implies a,b // c,d )
assume that
A1: X is being_plane and
A2: Y is being_plane and
A3: Z is being_plane and
A4: X '||' Y and
A5: X <> Y and
A6: a in X /\ Z and
A7: b in X /\ Z and
A8: c in Y /\ Z and
A9: d in Y /\ Z ; :: thesis: a,b // c,d
A10: c in Z by A8, XBOOLE_0:def 4;
A11: ( a in X & a in Z ) by A6, XBOOLE_0:def 4;
then A12: Z <> Y by A1, A2, A4, A5, Lm13;
A13: c in Y by A8, XBOOLE_0:def 4;
then A14: Z <> X by A1, A2, A4, A5, A10, Lm13;
set A = X /\ Z;
set C = Y /\ Z;
A15: ( b in X & b in Z ) by A7, XBOOLE_0:def 4;
A16: ( d in Y & d in Z ) by A9, XBOOLE_0:def 4;

now :: thesis: ( a <> b & c <> d implies a,b // c,d )

A17: ( Y /\ Z c= Y & Y /\ Z c= Z ) by XBOOLE_1:17;
set K = c * (X /\ Z);
assume that
A18: a <> b and
A19: c <> d ; :: thesis: a,b // c,d
A20: X /\ Z is being_line by A1, A3, A11, A15, A14, A18, Th24;
then A21: X /\ Z // c * (X /\ Z) by Def3;
X /\ Z c= X by XBOOLE_1:17;
then A22: c * (X /\ Z) c= Y by A4, A13, A20;
A23: c * (X /\ Z) c= Z by A3, A10, A20, Th28, XBOOLE_1:17;
( Y /\ Z is being_line & c * (X /\ Z) is being_line ) by A1, A2, A3, A11, A15, A13, A10, A16, A12, A14, A18, A19, Th24, Th27;
then c * (X /\ Z) = Y /\ Z by A2, A3, A12, A17, A23, A22, Th26;
hence a,b // c,d by A6, A7, A8, A9, A21, AFF_1:39; :: thesis: verum

end;

hence a,b // c,d by AFF_1:3; :: thesis: verum