let T be TopStruct ; :: thesis: for A being SubSpace of T
for F being Subset-Family of A holds F is Subset-Family of T
let A be SubSpace of T; :: thesis: for F being Subset-Family of A holds F is Subset-Family of T
let F be Subset-Family of A; :: thesis: F is Subset-Family of T
[#] A c= [#] T by PRE_TOPC:def 4;
then bool the carrier of A c= bool the carrier of T by ZFMISC_1:67;
hence F is Subset-Family of T by XBOOLE_1:1; :: thesis: verum