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 by A1, PRE_TOPC:def 2;
hence F is Subset of (InclPoset the topology of T) ; :: thesis: verum

end;

assume A2: 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 A2, PRE_TOPC:def 2; :: thesis: verum