let AS be AffinSpace; :: thesis: for a being Element of AS
for X, M, N 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; :: thesis: for X, M, N 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 X, M, N be Subset of AS; :: thesis: ( 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 & M c= X )
and
A3:
a in N
and
A4:
( M // N or N // M )
; :: thesis: N c= X
A5:
( M is being_line & N is being_line )
by A4, AFF_1:50;
consider K, P being Subset of AS such that
A6:
( K is being_line & P is being_line )
and
A7:
not K // P
and
A8:
X = Plane K,P
by A1, Def2;
now assume A10:
not
K // M
;
:: thesis: N c= Xthen A11:
X = Plane K,
M
by A2, A5, A6, A7, A8, Th20;
A12:
a in Plane K,
M
by A2, A5, A6, A7, A8, A10, Th20;
now assume A13:
M <> N
;
:: thesis: N c= Xconsider a' being
Element of
AS such that A14:
a,
a' // K
and A15:
a' in M
by A12, Lm3;
consider b' being
Element of
AS such that A16:
a' <> b'
and A17:
b' in M
by A5, AFF_1:32;
consider b being
Element of
AS such that A18:
(
a',
a // b',
b &
a',
b' // a,
b )
by DIRAF:47;
A19:
a <> a'
by A3, A4, A13, A15, AFF_1:59;
A20:
a <> b
proof
assume
a = b
;
:: thesis: contradiction
then
a,
a' // a,
b'
by A18, AFF_1:13;
then
LIN a,
a',
b'
by AFF_1:def 1;
then
LIN a',
b',
a
by AFF_1:15;
then
a in M
by A5, A15, A16, A17, AFF_1:39;
hence
contradiction
by A3, A4, A13, AFF_1:59;
:: thesis: verum
end;
a,
b // M
by A5, A15, A16, A17, A18, AFF_1:46, AFF_1:66;
then
a,
b // N
by A4, Th3;
then A21:
b in N
by A3, Th2;
b,
b' // K
by A14, A18, A19, Th4;
then
b in Plane K,
M
by A17;
hence
N c= X
by A2, A3, A5, A6, A11, A20, A21, Lm5;
:: thesis: verum end; hence
N c= X
by A2;
:: thesis: verum end;
hence
N c= X
by A9; :: thesis: verum