let X be TopSpace; :: thesis: for Y being SubSpace of X

for Z being SubSpace of Y

for A being Subset of Z holds A is Subset of X

let Y be SubSpace of X; :: thesis: for Z being SubSpace of Y

for A being Subset of Z holds A is Subset of X

let Z be SubSpace of Y; :: thesis: for A being Subset of Z holds A is Subset of X

let A be Subset of Z; :: thesis: A is Subset of X

the carrier of Z is Subset of Y by TSEP_1:1;

then A1: A is Subset of Y by XBOOLE_1:1;

the carrier of Y is Subset of X by TSEP_1:1;

hence A is Subset of X by A1, XBOOLE_1:1; :: thesis: verum

for Z being SubSpace of Y

for A being Subset of Z holds A is Subset of X

let Y be SubSpace of X; :: thesis: for Z being SubSpace of Y

for A being Subset of Z holds A is Subset of X

let Z be SubSpace of Y; :: thesis: for A being Subset of Z holds A is Subset of X

let A be Subset of Z; :: thesis: A is Subset of X

the carrier of Z is Subset of Y by TSEP_1:1;

then A1: A is Subset of Y by XBOOLE_1:1;

the carrier of Y is Subset of X by TSEP_1:1;

hence A is Subset of X by A1, XBOOLE_1:1; :: thesis: verum