let T be non empty TopSpace; :: thesis: 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 #) )
let F be set ; :: thesis: ( F is open Subset-Family of T iff F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #) )
thus ( F is open Subset-Family of T implies F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #) ) :: thesis: ( F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #) implies F is open Subset-Family of T )

proof

assume A1: F is open Subset-Family of T ; :: thesis: F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #)
then reconsider F = F as Subset-Family of TopStruct(# the carrier of T, the topology of T #) ;
F is open by A1, TOPS_2:def 1, PRE_TOPC:30;
hence F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #) ; :: thesis: verum

end;

assume A2: F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #) ; :: thesis: F is open Subset-Family of T
then reconsider F = F as Subset-Family of T ;
F is open by A2, TOPS_2:def 1, PRE_TOPC:30;
hence F is open Subset-Family of T ; :: thesis: verum