let X be non empty TopSpace; :: thesis: for P being Subset of X st P is open holds
MaxADSet P = P
let P be Subset of X; :: thesis: ( P is open implies MaxADSet P = P )
set F = { G where G is Subset of X : ( G is open & P c= G ) } ;
A1: P c= MaxADSet P by Th32;
assume P is open ; :: thesis: MaxADSet P = P
then P in { G where G is Subset of X : ( G is open & P c= G ) } ;
then A2: meet { G where G is Subset of X : ( G is open & P c= G ) } c= P by SETFAM_1:3;
MaxADSet P c= meet { G where G is Subset of X : ( G is open & P c= G ) } by Th55;
then MaxADSet P c= P by A2;
hence MaxADSet P = P by A1; :: thesis: verum