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 )

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

( 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 A2:
F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #)
; :: thesis: F is open Subset-Family of T
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;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

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