let AS be AffinSpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 :: thesis: ( 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 ; :: thesis: X = Y
consider 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 :: thesis: ( b <> q implies X = Y )

assume b <> q ; :: thesis: X = Y
then not LIN b,q,p by A3, A9, A12, A16, Lm7;
hence X = Y by A1, A2, A5, A6, A9, A12, A15, Th25; :: thesis: verum

end;

now :: thesis: ( a <> q implies X = Y )

assume a <> q ; :: thesis: X = Y
then not LIN a,q,p by A3, A8, A12, A16, Lm7;
hence X = Y by A1, A2, A5, A6, A8, A12, A15, Th25; :: thesis: verum

end;

hence X = Y by A10, A17; :: thesis: 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 :: thesis: ( M // N implies X = Y )

assume M // N ; :: thesis: X = Y
then 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; :: thesis: verum

end;

hence X = Y by A1, A3, A4, A5, A11, Th22; :: thesis: verum