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

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