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

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