let Y be non empty TopSpace; :: thesis: for x being Point of Y holds MaxADSet x c= meet { G where G is Subset of Y : ( G is open & x in G ) }
let x be Point of Y; :: thesis: MaxADSet x c= meet { G where G is Subset of Y : ( G is open & x in G ) }
set F = { G where G is Subset of Y : ( G is open & x in G ) } ;
[#] Y in { G where G is Subset of Y : ( G is open & x in G ) } ;
then A1: { G where G is Subset of Y : ( G is open & x in G ) } <> {} ;
{ G where G is Subset of Y : ( G is open & x in G ) } c= bool the carrier of Y
proof
let C be object ; :: according to TARSKI:def 3 :: thesis: ( not C in { G where G is Subset of Y : ( G is open & x in G ) } or C in bool the carrier of Y )
assume C in { G where G is Subset of Y : ( G is open & x in G ) } ; :: thesis: C in bool the carrier of Y
then ex P being Subset of Y st
( C = P & P is open & x in P ) ;
hence C in bool the carrier of Y ; :: thesis: verum
end;
then reconsider F = { G where G is Subset of Y : ( G is open & x in G ) } as Subset-Family of Y ;
now :: thesis: for C being set st C in F holds
MaxADSet x c= C
let C be set ; :: thesis: ( C in F implies MaxADSet x c= C )
assume C in F ; :: thesis:
then ex G being Subset of Y st
( G = C & G is open & x in G ) ;
hence MaxADSet x c= C by Th24; :: thesis: verum
end;
hence MaxADSet x c= meet { G where G is Subset of Y : ( G is open & x in G ) } by ; :: thesis: verum