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 Z: 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

proof

let P be Subset of TopStruct(# the carrier of T,the topology of T #); :: according to TOPS_2:def 1 :: thesis: ( not P in F or P is open )
assume ZZ: P in F ; :: thesis: P is open
P is open Subset of T by ZZ, Z, TOPS_2:def 1;
hence P is open by ZZ, PRE_TOPC:60; :: thesis: verum

end;

hence F is open Subset-Family of TopStruct(# the carrier of T,the topology of T #) ; :: thesis: verum

end;

assume Z: 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

proof

let P be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not P in F or P is open )
assume ZZ: P in F ; :: thesis: P is open
P is open Subset of TopStruct(# the carrier of T,the topology of T #) by ZZ, Z, TOPS_2:def 1;
hence P is open by ZZ, PRE_TOPC:60; :: thesis: verum

end;

hence F is open Subset-Family of T ; :: thesis: verum