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

hereby :: thesis: ( F is Subset of implies F is open )

assume A1: F is open ; :: thesis: F is Subset of
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 a' = a as Subset of ;
a' is open by A1, A2, TOPS_2:def 1;
hence a in the topology of T by PRE_TOPC:def 5; :: thesis: verum

end;

hence F is Subset of ; :: thesis: verum

end;

assume A3: F is Subset of ; :: thesis: F is open
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
hence P is open by A3, PRE_TOPC:def 5; :: thesis: verum