let AS be AffinSpace; for X, Y being Subset of AS st X is being_plane & Y is being_plane holds
( X '||' Y iff ex A, P, M, N being Subset of AS st
( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) ) )
let X, Y be Subset of AS; ( X is being_plane & Y is being_plane implies ( X '||' Y iff ex A, P, M, N being Subset of AS st
( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) ) ) )
assume that
A1:
X is being_plane
and
A2:
Y is being_plane
; ( X '||' Y iff ex A, P, M, N being Subset of AS st
( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) ) )
A3:
now ( ex A, P, M, N being Subset of AS st
( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) ) implies X '||' Y )given A,
P,
M,
N being
Subset of
AS such that A4:
not
A // P
and A5:
A c= X
and A6:
P c= X
and A7:
M c= Y
and A8:
N c= Y
and A9:
(
A // M or
M // A )
and A10:
(
P // N or
N // P )
;
X '||' YA11:
M is
being_line
by A9, AFF_1:36;
A12:
not
M // N
N is
being_line
by A10, AFF_1:36;
then consider q being
Element of
AS such that A13:
q in M
and A14:
q in N
by A2, A7, A8, A11, A12, Th22;
A15:
A is
being_line
by A9, AFF_1:36;
A16:
P is
being_line
by A10, AFF_1:36;
then consider p being
Element of
AS such that A17:
p in A
and A18:
p in P
by A1, A4, A5, A6, A15, Th22;
now for a being Element of AS
for Z being Subset of AS st a in Y & Z is being_line & Z c= X holds
a * Z c= Ylet a be
Element of
AS;
for Z being Subset of AS st a in Y & Z is being_line & Z c= X holds
a * Z c= Ylet Z be
Subset of
AS;
( a in Y & Z is being_line & Z c= X implies a * Z c= Y )assume that A19:
a in Y
and A20:
Z is
being_line
and A21:
Z c= X
;
a * Z c= YA22:
a in a * Z
by A20, Def3;
A23:
Z // a * Z
by A20, Def3;
A24:
now ( Z // P implies a * Z c= Y )end; A25:
now ( not Z // A & not Z // P implies a * Z c= Y )assume that A26:
not
Z // A
and A27:
not
Z // P
;
a * Z c= Yconsider b being
Element of
AS such that A28:
p <> b
and A29:
b in A
by A15, AFF_1:20;
set Z1 =
b * Z;
A30:
b * Z is
being_line
by A20, Th27;
A31:
not
b * Z // P
A33:
Z // b * Z
by A20, Def3;
b * Z c= X
by A1, A5, A20, A21, A29, Th28;
then consider c being
Element of
AS such that A34:
c in b * Z
and A35:
c in P
by A1, A6, A16, A30, A31, Th22;
A36:
b in b * Z
by A20, Def3;
then A37:
p <> c
by A15, A17, A26, A28, A29, A30, A33, A34, AFF_1:18;
A38:
A <> P
by A4, A15, AFF_1:41;
A39:
not
LIN p,
b,
c
proof
assume
LIN p,
b,
c
;
contradiction
then
c in A
by A15, A17, A28, A29, AFF_1:25;
hence
contradiction
by A15, A16, A17, A18, A35, A37, A38, AFF_1:18;
verum
end; then A40:
b <> c
by AFF_1:7;
consider b9 being
Element of
AS such that A41:
q <> b9
and A42:
b9 in M
by A11, AFF_1:20;
p,
b // q,
b9
by A9, A17, A13, A29, A42, AFF_1:39;
then consider c9 being
Element of
AS such that A43:
p,
c // q,
c9
and A44:
b,
c // b9,
c9
by A41, A39, Th54;
set Z2 =
Line (
b9,
c9);
A45:
(
b9 in Line (
b9,
c9) &
c9 in Line (
b9,
c9) )
by AFF_1:15;
A46:
b9 <> c9
proof
assume A47:
b9 = c9
;
contradiction
q,
b9 // M
by A11, A13, A42, AFF_1:52;
then
p,
c // M
by A41, A43, A47, Th4;
then
p,
c // A
by A9, Th3;
then
c in A
by A17, Th2;
hence
contradiction
by A15, A16, A17, A18, A35, A37, A38, AFF_1:18;
verum
end; then
Line (
b9,
c9) is
being_line
by AFF_1:def 3;
then
b * Z // Line (
b9,
c9)
by A30, A36, A34, A44, A40, A46, A45, AFF_1:38;
then
Z // Line (
b9,
c9)
by A33, AFF_1:44;
then A48:
a * Z // Line (
b9,
c9)
by A23, AFF_1:44;
c9 in N
by A10, A18, A14, A35, A37, A43, Th7;
then
Line (
b9,
c9)
c= Y
by A2, A7, A8, A42, A46, Th19;
hence
a * Z c= Y
by A2, A19, A22, A48, Th23;
verum end; hence
a * Z c= Y
by A24, A25;
verum end; hence
X '||' Y
;
verum end;
now ( X '||' Y implies ex A, P being Element of K24( the carrier of AS) ex M, N being Subset of AS st
( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) ) )consider a9,
b9,
c9 being
Element of
AS such that A49:
a9 in Y
and
b9 in Y
and
c9 in Y
and
not
LIN a9,
b9,
c9
by A2, Th34;
assume A50:
X '||' Y
;
ex A, P being Element of K24( the carrier of AS) ex M, N being Subset of AS st
( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) )consider a,
b,
c being
Element of
AS such that A51:
a in X
and A52:
b in X
and A53:
c in X
and A54:
not
LIN a,
b,
c
by A1, Th34;
set A =
Line (
a,
b);
set P =
Line (
a,
c);
A55:
(
b in Line (
a,
b) &
c in Line (
a,
c) )
by AFF_1:15;
A56:
a <> c
by A54, AFF_1:7;
then A57:
Line (
a,
c)
c= X
by A1, A51, A53, Th19;
take A =
Line (
a,
b);
ex P being Element of K24( the carrier of AS) ex M, N being Subset of AS st
( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) )take P =
Line (
a,
c);
ex M, N being Subset of AS st
( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) )take M =
a9 * A;
ex N being Subset of AS st
( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) )take N =
a9 * P;
( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) )A58:
a in A
by AFF_1:15;
A59:
a <> b
by A54, AFF_1:7;
then A60:
A is
being_line
by AFF_1:def 3;
A61:
a in P
by AFF_1:15;
A62:
not
A // P
A63:
P is
being_line
by A56, AFF_1:def 3;
A c= X
by A1, A51, A52, A59, Th19;
hence
( not
A // P &
A c= X &
P c= X &
M c= Y &
N c= Y & (
A // M or
M // A ) & (
P // N or
N // P ) )
by A50, A60, A63, A49, A62, A57, Def3;
verum end;
hence
( X '||' Y iff ex A, P, M, N being Subset of AS st
( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) ) )
by A3; verum