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