let AS be AffinSpace; for a being Element of AS
for M, N, X being Subset of AS st X is being_plane & a in X & M c= X & a in N & ( M // N or N // M ) holds
N c= X
let a be Element of AS; for M, N, X being Subset of AS st X is being_plane & a in X & M c= X & a in N & ( M // N or N // M ) holds
N c= X
let M, N, X be Subset of AS; ( X is being_plane & a in X & M c= X & a in N & ( M // N or N // M ) implies N c= X )
assume that
A1:
X is being_plane
and
A2:
a in X
and
A3:
M c= X
and
A4:
a in N
and
A5:
( M // N or N // M )
; N c= X
A6:
M is being_line
by A5, AFF_1:36;
consider K, P being Subset of AS such that
A7:
K is being_line
and
A8:
P is being_line
and
not K // P
and
A9:
X = Plane (K,P)
by A1;
A10:
N is being_line
by A5, AFF_1:36;
A11:
now ( not K // M implies N c= X )assume A12:
not
K // M
;
N c= Xthen A13:
X = Plane (
K,
M)
by A3, A6, A7, A8, A9, Th20;
A14:
a in Plane (
K,
M)
by A2, A3, A6, A7, A8, A9, A12, Th20;
now ( M <> N implies N c= X )consider a9 being
Element of
AS such that A15:
a,
a9 // K
and A16:
a9 in M
by A14, Lm3;
consider b9 being
Element of
AS such that A17:
a9 <> b9
and A18:
b9 in M
by A6, AFF_1:20;
consider b being
Element of
AS such that A19:
a9,
a // b9,
b
and A20:
a9,
b9 // a,
b
by DIRAF:40;
assume A21:
M <> N
;
N c= Xthen
a <> a9
by A4, A5, A16, AFF_1:45;
then
b,
b9 // K
by A15, A19, Th4;
then A22:
b in Plane (
K,
M)
by A18;
A23:
a <> b
proof
assume
a = b
;
contradiction
then
a,
a9 // a,
b9
by A19, AFF_1:4;
then
LIN a,
a9,
b9
by AFF_1:def 1;
then
LIN a9,
b9,
a
by AFF_1:6;
then
a in M
by A6, A16, A17, A18, AFF_1:25;
hence
contradiction
by A4, A5, A21, AFF_1:45;
verum
end;
a,
b // M
by A6, A16, A17, A18, A20, AFF_1:32, AFF_1:52;
then
a,
b // N
by A5, Th3;
then
b in N
by A4, Th2;
hence
N c= X
by A2, A4, A6, A10, A7, A13, A23, A22, Lm5;
verum end; hence
N c= X
by A3;
verum end;
hence
N c= X
by A11; verum