set F = { G where G is Subset of X : ( G is open & x in G ) } ;

{ G where G is Subset of X : ( G is open & x in G ) } c= bool the carrier of X

A1: MaxADSet x c= Cl {x} by Th48;

A2: (Cl {x}) /\ (meet F) c= MaxADSet x

then MaxADSet x c= (Cl {x}) /\ (meet F) by A1, XBOOLE_1:19;

hence for b_{1} being non empty Subset of X holds

( b_{1} = MaxADSet x iff b_{1} = (Cl {x}) /\ (meet { G where G is Subset of X : ( G is open & x in G ) } ) )
by A2; :: thesis: verum

{ G where G is Subset of X : ( G is open & x in G ) } c= bool the carrier of X

proof

then reconsider F = { G where G is Subset of X : ( G is open & x in G ) } as Subset-Family of X ;
let C be object ; :: according to TARSKI:def 3 :: thesis: ( not C in { G where G is Subset of X : ( G is open & x in G ) } or C in bool the carrier of X )

assume C in { G where G is Subset of X : ( G is open & x in G ) } ; :: thesis: C in bool the carrier of X

then ex P being Subset of X st

( C = P & P is open & x in P ) ;

hence C in bool the carrier of X ; :: thesis: verum

end;assume C in { G where G is Subset of X : ( G is open & x in G ) } ; :: thesis: C in bool the carrier of X

then ex P being Subset of X st

( C = P & P is open & x in P ) ;

hence C in bool the carrier of X ; :: thesis: verum

A1: MaxADSet x c= Cl {x} by Th48;

A2: (Cl {x}) /\ (meet F) c= MaxADSet x

proof

MaxADSet x c= meet F
by Th46;
assume
not (Cl {x}) /\ (meet F) c= MaxADSet x
; :: thesis: contradiction

then ((Cl {x}) /\ (meet F)) \ (MaxADSet x) <> {} by XBOOLE_1:37;

then consider a being object such that

A3: a in ((Cl {x}) /\ (meet F)) \ (MaxADSet x) by XBOOLE_0:def 1;

A4: a in (Cl {x}) /\ (meet F) by A3, XBOOLE_0:def 5;

reconsider a = a as Point of X by A3;

not a in MaxADSet x by A3, XBOOLE_0:def 5;

then A5: MaxADSet a <> MaxADSet x by Th21;

then A8: Cl {x} c= Cl {a} by TOPS_1:5;

a in Cl {x} by A4, XBOOLE_0:def 4;

then {a} c= Cl {x} by ZFMISC_1:31;

then Cl {a} c= Cl {x} by TOPS_1:5;

then Cl {x} = Cl {a} by A8;

hence contradiction by A5, Th49; :: thesis: verum

end;then ((Cl {x}) /\ (meet F)) \ (MaxADSet x) <> {} by XBOOLE_1:37;

then consider a being object such that

A3: a in ((Cl {x}) /\ (meet F)) \ (MaxADSet x) by XBOOLE_0:def 1;

A4: a in (Cl {x}) /\ (meet F) by A3, XBOOLE_0:def 5;

reconsider a = a as Point of X by A3;

not a in MaxADSet x by A3, XBOOLE_0:def 5;

then A5: MaxADSet a <> MaxADSet x by Th21;

now :: thesis: x in Cl {a}

then
{x} c= Cl {a}
by ZFMISC_1:31;set G = (Cl {a}) ` ;

{a} c= Cl {a} by PRE_TOPC:18;

then A6: a in Cl {a} by ZFMISC_1:31;

assume not x in Cl {a} ; :: thesis: contradiction

then x in (Cl {a}) ` by SUBSET_1:29;

then (Cl {a}) ` in F ;

then A7: meet F c= (Cl {a}) ` by SETFAM_1:3;

a in meet F by A4, XBOOLE_0:def 4;

hence contradiction by A7, A6, XBOOLE_0:def 5; :: thesis: verum

end;{a} c= Cl {a} by PRE_TOPC:18;

then A6: a in Cl {a} by ZFMISC_1:31;

assume not x in Cl {a} ; :: thesis: contradiction

then x in (Cl {a}) ` by SUBSET_1:29;

then (Cl {a}) ` in F ;

then A7: meet F c= (Cl {a}) ` by SETFAM_1:3;

a in meet F by A4, XBOOLE_0:def 4;

hence contradiction by A7, A6, XBOOLE_0:def 5; :: thesis: verum

then A8: Cl {x} c= Cl {a} by TOPS_1:5;

a in Cl {x} by A4, XBOOLE_0:def 4;

then {a} c= Cl {x} by ZFMISC_1:31;

then Cl {a} c= Cl {x} by TOPS_1:5;

then Cl {x} = Cl {a} by A8;

hence contradiction by A5, Th49; :: thesis: verum

then MaxADSet x c= (Cl {x}) /\ (meet F) by A1, XBOOLE_1:19;

hence for b

( b