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