let T be TopStruct ; :: thesis: for X9 being SubSpace of T
for A being Subset of X9 holds A is Subset of T
let X9 be SubSpace of T; :: thesis: for A being Subset of X9 holds A is Subset of T
let A be Subset of X9; :: thesis: A is Subset of T
[#] X9 c= [#] T by Def4;
hence A is Subset of T by XBOOLE_1:1; :: thesis: verum