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)) \ () <> {} by XBOOLE_1:37;
then consider a being object such that
A3: a in ((Cl {x}) /\ (meet F)) \ () by XBOOLE_0:def 1;
A4: a in (Cl {x}) /\ (meet F) by ;
reconsider a = a as Point of X by A3;
not a in MaxADSet x by ;
then A5: MaxADSet a <> MaxADSet x by Th21;
now :: thesis: x in Cl {a}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 ;
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 ;
hence for b1 being non empty Subset of X holds
( b1 = MaxADSet x iff b1 = (Cl {x}) /\ (meet { G where G is Subset of X : ( G is open & x in G ) } ) ) by A2; :: thesis: verum