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;

A18: c in N and

d in N and

c <> d by A4, AFF_1:19;

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 )

consider c, d being Element of AS such that ( 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;

end;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;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

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

hence
X = Y
by A10, A17; :: thesis: verumassume
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;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

A18: c in N and

d in N and

c <> d by A4, AFF_1:19;

now :: thesis: ( M // N implies X = Y )

hence
X = Y
by A1, A3, A4, A5, A11, Th22; :: thesis: verumassume
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;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