thus ( M is maximal_T_0 implies ( M is T_0 & MaxADSet M = the carrier of X ) ) :: thesis: ( M is T_0 & MaxADSet M = the carrier of X implies M is maximal_T_0 )
proof
assume A1: M is maximal_T_0 ; :: thesis: ( M is T_0 & MaxADSet M = the carrier of X )
hence A2: M is T_0 ; :: thesis: MaxADSet M = the carrier of X
the carrier of X c= MaxADSet M
proof
assume not the carrier of X c= MaxADSet M ; :: thesis: contradiction
then consider x being object such that
A3: x in the carrier of X and
A4: not x in MaxADSet M by TARSKI:def 3;
reconsider x = x as Point of X by A3;
set A = M \/ {x};
for a being Point of X st a in M \/ {x} holds
(M \/ {x}) /\ (MaxADSet a) = {a}
proof
let a be Point of X; :: thesis: ( a in M \/ {x} implies (M \/ {x}) /\ (MaxADSet a) = {a} )
assume a in M \/ {x} ; :: thesis: (M \/ {x}) /\ (MaxADSet a) = {a}
then A5: ( a in M or a in {x} ) by XBOOLE_0:def 3;
now :: thesis: (M \/ {x}) /\ (MaxADSet a) = {a}
per cases ( a in M or a = x ) by A5, TARSKI:def 1;
end;
end;
hence (M \/ {x}) /\ (MaxADSet a) = {a} ; :: thesis: verum
end;
then A12: M \/ {x} is T_0 ;
A13: M c= MaxADSet M by TEX_4:32;
A14: {x} c= M \/ {x} by XBOOLE_1:7;
M c= M \/ {x} by XBOOLE_1:7;
then M = M \/ {x} by A1, A12;
then x in M by A14, ZFMISC_1:31;
hence contradiction by A4, A13; :: thesis: verum
end;
hence MaxADSet M = the carrier of X by XBOOLE_0:def 10; :: thesis: verum
end;
assume A15: M is T_0 ; :: thesis: ( not MaxADSet M = the carrier of X or M is maximal_T_0 )
assume A16: MaxADSet M = the carrier of X ; :: thesis: 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; :: thesis: ( D is T_0 & M c= D implies M = D )
assume A17: D is T_0 ; :: thesis: ( not M c= D or M = D )
assume A18: M c= D ; :: thesis: M = D
D c= M
proof
assume not D c= M ; :: thesis: 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; :: thesis: verum
end;
hence M = D by A18, XBOOLE_0:def 10; :: thesis: verum
end;
hence M is maximal_T_0 by A15; :: thesis: verum