for T being TopStruct
for A being SubSpace of T
for F being Subset-Family of A holds F is Subset-Family of T