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;

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 )

hence
a,b // c,d
by AFF_1:3; :: thesis: verumA17:
( 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;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