for T being TopStruct
for A being SubSpace of T
for B being Subset of A holds
( B is open iff ex C being Subset of T st
( C is open & C /\ ([#] A) = B ) )