let AS be AffinSpace; 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; 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; ( 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
; 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; verum