let X be non empty TopSpace; :: thesis: for X0 being closed 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 closed 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 closed by TSEP_1:11;

assume A is Subset of X0 ; :: thesis: MaxADSspace A is SubSpace of X0

then MaxADSet A c= D by A1, Th40;

then the carrier of (MaxADSspace A) c= the carrier of X0 by Def18;

hence MaxADSspace A is SubSpace of X0 by Lm2; :: thesis: verum

for A being non empty Subset of X st A is Subset of X0 holds

MaxADSspace A is SubSpace of X0

let X0 be closed 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 closed by TSEP_1:11;

assume A is Subset of X0 ; :: thesis: MaxADSspace A is SubSpace of X0

then MaxADSet A c= D by A1, Th40;

then the carrier of (MaxADSspace A) c= the carrier of X0 by Def18;

hence MaxADSspace A is SubSpace of X0 by Lm2; :: thesis: verum