let X be non empty TopSpace; :: thesis: for X0 being open SubSpace of X
for A being non empty Subset of X st A is Subset of X0 holds
MaxADSspace A is SubSpace of X0
let X0 be open SubSpace of X; :: thesis: for A being non empty Subset of X st A is Subset of X0 holds
MaxADSspace A is SubSpace of X0
let A be non empty Subset of X; :: thesis: ( A is Subset of X0 implies MaxADSspace A is SubSpace of X0 )
reconsider D = the carrier of X0 as Subset of X by TSEP_1:1;
A1: D is open by TSEP_1:16;
assume A is Subset of X0 ; :: thesis: MaxADSspace A is SubSpace of X0
then MaxADSet A c= D by A1, Th38;
then the carrier of (MaxADSspace A) c= the carrier of X0 by Def18;
hence MaxADSspace A is SubSpace of X0 by Lm2; :: thesis: verum