let T be TopSpace; :: thesis: for F being Subset-Family of T holds
( F is open iff F is Subset of (InclPoset the topology of T) )
let F be Subset-Family of T; :: thesis: ( F is open iff F is Subset of (InclPoset the topology of T) )

hereby :: thesis: ( F is Subset of (InclPoset the topology of T) implies F is open )

assume A1: F is open ; :: thesis: F is Subset of (InclPoset the topology of T)
F c= the topology of T

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in F or a in the topology of T )
assume A2: a in F ; :: thesis: a in the topology of T
then reconsider a9 = a as Subset of T ;
a9 is open by A1, A2, TOPS_2:def 1;
hence a in the topology of T by PRE_TOPC:def 2; :: thesis: verum

end;

hence F is Subset of (InclPoset the topology of T) ; :: thesis: verum

end;

assume A3: F is Subset of (InclPoset the topology of T) ; :: thesis: F is open
let P be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not P in F or P is open )
assume P in F ; :: thesis: P is open
hence P is open by A3, PRE_TOPC:def 2; :: thesis: verum