let AS be AffinSpace; for M, N, X, Y being Subset of AS st X is being_plane & Y is being_plane & M is being_line & N is being_line & M c= X & N c= X & M c= Y & N c= Y & M <> N holds
X = Y
let M, N, X, Y be Subset of AS; ( X is being_plane & Y is being_plane & M is being_line & N is being_line & M c= X & N c= X & M c= Y & N c= Y & M <> N implies X = Y )
assume that
A1:
X is being_plane
and
A2:
Y is being_plane
and
A3:
M is being_line
and
A4:
N is being_line
and
A5:
( M c= X & N c= X )
and
A6:
( M c= Y & N c= Y )
and
A7:
M <> N
; X = Y
consider a, b being Element of AS such that
A8:
a in M
and
A9:
b in M
and
A10:
a <> b
by A3, AFF_1:19;
A11:
now ( ex q being Element of AS st
( q in M & q in N ) implies X = Y )given q being
Element of
AS such that A12:
q in M
and A13:
q in N
;
X = Yconsider p being
Element of
AS such that A14:
q <> p
and A15:
p in N
by A4, AFF_1:20;
A16:
not
p in M
by A3, A4, A7, A12, A13, A14, A15, AFF_1:18;
A17:
now ( b <> q implies X = Y )assume
b <> q
;
X = Ythen
not
LIN b,
q,
p
by A3, A9, A12, A16, Lm7;
hence
X = Y
by A1, A2, A5, A6, A9, A12, A15, Th25;
verum end; now ( a <> q implies X = Y )assume
a <> q
;
X = Ythen
not
LIN a,
q,
p
by A3, A8, A12, A16, Lm7;
hence
X = Y
by A1, A2, A5, A6, A8, A12, A15, Th25;
verum end; hence
X = Y
by A10, A17;
verum end;
consider c, d being Element of AS such that
A18:
c in N
and
d in N
and
c <> d
by A4, AFF_1:19;
now ( M // N implies X = Y )assume
M // N
;
X = Ythen
not
c in M
by A7, A18, AFF_1:45;
then
not
LIN a,
b,
c
by A3, A8, A9, A10, Lm7;
hence
X = Y
by A1, A2, A5, A6, A8, A9, A18, Th25;
verum end;
hence
X = Y
by A1, A3, A4, A5, A11, Th22; verum