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 & 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; 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; ( 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
; 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 ( 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
;
a,b // c,dA20:
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;
verum end;
hence
a,b // c,d
by AFF_1:3; verum