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

proof

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;

then reconsider F = { G where G is Subset of X : ( G is open & x in G ) } as Subset-Family of X ;
A1: MaxADSet x c= Cl {x} by Th48;
A2: (Cl {x}) /\ (meet F) c= MaxADSet x

proof

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;

now :: thesis: x in Cl {a}

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;

then {x} c= Cl {a} by ZFMISC_1:31;
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;

MaxADSet x c= meet F by Th46;
then MaxADSet x c= (Cl {x}) /\ (meet F) by A1, XBOOLE_1:19;
hence for b₁ being non empty Subset of X holds
( b₁ = MaxADSet x iff b₁ = (Cl {x}) /\ (meet { G where G is Subset of X : ( G is open & x in G ) } ) ) by A2; :: thesis: verum