thus
( M is maximal_T_0 implies ( M is T_0 & MaxADSet M = the carrier of X ) )
( M is T_0 & MaxADSet M = the carrier of X implies M is maximal_T_0 )
assume A15:
M is T_0
; ( not MaxADSet M = the carrier of X or M is maximal_T_0 )
assume A16:
MaxADSet M = the carrier of X
; M is maximal_T_0
for D being Subset of X st D is T_0 & M c= D holds
M = D
proof
let D be
Subset of
X;
( D is T_0 & M c= D implies M = D )
assume A17:
D is
T_0
;
( not M c= D or M = D )
assume A18:
M c= D
;
M = D
D c= M
proof
assume
not
D c= M
;
contradiction
then consider x being
object such that A19:
x in D
and A20:
not
x in M
by TARSKI:def 3;
A21:
x in the
carrier of
X
by A19;
reconsider x =
x as
Point of
X by A19;
x in union { (MaxADSet a) where a is Point of X : a in M }
by A16, A21, TEX_4:def 11;
then consider C being
set such that A22:
x in C
and A23:
C in { (MaxADSet a) where a is Point of X : a in M }
by TARSKI:def 4;
consider a being
Point of
X such that A24:
C = MaxADSet a
and A25:
a in M
by A23;
M /\ (MaxADSet x) c= D /\ (MaxADSet x)
by A18, XBOOLE_1:26;
then A26:
M /\ (MaxADSet x) c= {x}
by A17, A19;
MaxADSet a = MaxADSet x
by A22, A24, TEX_4:21;
then
M /\ (MaxADSet x) = {a}
by A15, A25;
hence
contradiction
by A20, A25, A26, ZFMISC_1:18;
verum
end;
hence
M = D
by A18, XBOOLE_0:def 10;
verum
end;
hence
M is maximal_T_0
by A15; verum