theorem Th22: :: COMPTS_1:22

for T being non empty TopSpace
for F being set holds
( F is open Subset-Family of T iff F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #) )