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