let T be non empty TopSpace; :: thesis: for F being set holds
( F is open Subset-Family of iff F is open Subset-Family of )
let F be set ; :: thesis: ( F is open Subset-Family of iff F is open Subset-Family of )
thus ( F is open Subset-Family of implies F is open Subset-Family of ) :: thesis: ( F is open Subset-Family of implies F is open Subset-Family of )

proof

assume A1: F is open Subset-Family of ; :: thesis: F is open Subset-Family of
then reconsider F = F as Subset-Family of ;
F is open

proof

let P be Subset of ; :: according to TOPS_2:def 1 :: thesis: ( not P in F or P is open )
assume P in F ; :: thesis: P is open
then P is open Subset of by A1, TOPS_2:def 1;
hence P is open by PRE_TOPC:60; :: thesis: verum

end;

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

end;

assume A2: F is open Subset-Family of ; :: thesis: F is open Subset-Family of
then reconsider F = F as Subset-Family of ;
F is open

proof

let P be Subset of ; :: according to TOPS_2:def 1 :: thesis: ( not P in F or P is open )
assume P in F ; :: thesis: P is open
then P is open Subset of by A2, TOPS_2:def 1;
hence P is open by PRE_TOPC:60; :: thesis: verum

end;

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