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