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 & a in X /\ Z & b in X /\ Z & c in Y /\ Z & d in Y /\ Z & X <> Y & a <> b & c <> d holds

X /\ Z // Y /\ Z

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 & a in X /\ Z & b in X /\ Z & c in Y /\ Z & d in Y /\ Z & X <> Y & a <> b & c <> d holds

X /\ Z // Y /\ Z

let X, Y, Z be Subset of AS; :: thesis: ( X is being_plane & Y is being_plane & Z is being_plane & X '||' Y & a in X /\ Z & b in X /\ Z & c in Y /\ Z & d in Y /\ Z & X <> Y & a <> b & c <> d implies X /\ Z // Y /\ Z )

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: a in X /\ Z and

A6: b in X /\ Z and

A7: c in Y /\ Z and

A8: d in Y /\ Z and

A9: X <> Y and

A10: a <> b and

A11: c <> d ; :: thesis: X /\ Z // Y /\ Z

A12: ( d in Y & d in Z ) by A8, XBOOLE_0:def 4;

set A = X /\ Z;

set C = Y /\ Z;

A13: ( c in Y & c in Z ) by A7, XBOOLE_0:def 4;

A14: ( a in X & a in Z ) by A5, XBOOLE_0:def 4;

then Z <> Y by A1, A2, A4, A9, Lm13;

then A15: Y /\ Z is being_line by A2, A3, A11, A13, A12, Th24;

A16: ( b in X & b in Z ) by A6, XBOOLE_0:def 4;

Z <> X by A1, A2, A4, A9, A13, Lm13;

then A17: X /\ Z is being_line by A1, A3, A10, A14, A16, Th24;

a,b // c,d by A1, A2, A3, A4, A5, A6, A7, A8, A9, Th63;

hence X /\ Z // Y /\ Z by A5, A6, A7, A8, A10, A11, A17, A15, AFF_1:38; :: thesis: verum

for X, Y, Z being Subset of AS st X is being_plane & Y is being_plane & Z is being_plane & X '||' Y & a in X /\ Z & b in X /\ Z & c in Y /\ Z & d in Y /\ Z & X <> Y & a <> b & c <> d holds

X /\ Z // Y /\ Z

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 & a in X /\ Z & b in X /\ Z & c in Y /\ Z & d in Y /\ Z & X <> Y & a <> b & c <> d holds

X /\ Z // Y /\ Z

let X, Y, Z be Subset of AS; :: thesis: ( X is being_plane & Y is being_plane & Z is being_plane & X '||' Y & a in X /\ Z & b in X /\ Z & c in Y /\ Z & d in Y /\ Z & X <> Y & a <> b & c <> d implies X /\ Z // Y /\ Z )

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: a in X /\ Z and

A6: b in X /\ Z and

A7: c in Y /\ Z and

A8: d in Y /\ Z and

A9: X <> Y and

A10: a <> b and

A11: c <> d ; :: thesis: X /\ Z // Y /\ Z

A12: ( d in Y & d in Z ) by A8, XBOOLE_0:def 4;

set A = X /\ Z;

set C = Y /\ Z;

A13: ( c in Y & c in Z ) by A7, XBOOLE_0:def 4;

A14: ( a in X & a in Z ) by A5, XBOOLE_0:def 4;

then Z <> Y by A1, A2, A4, A9, Lm13;

then A15: Y /\ Z is being_line by A2, A3, A11, A13, A12, Th24;

A16: ( b in X & b in Z ) by A6, XBOOLE_0:def 4;

Z <> X by A1, A2, A4, A9, A13, Lm13;

then A17: X /\ Z is being_line by A1, A3, A10, A14, A16, Th24;

a,b // c,d by A1, A2, A3, A4, A5, A6, A7, A8, A9, Th63;

hence X /\ Z // Y /\ Z by A5, A6, A7, A8, A10, A11, A17, A15, AFF_1:38; :: thesis: verum