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