let T be TopSpace; :: thesis: for X being set holds
( X is open Subset of iff X is open Subset of )
let X be set ; :: thesis: ( X is open Subset of iff X is open Subset of )
( X in the topology of T iff X in the topology of TopStruct(# the carrier of T,the topology of T #) ) ;
hence ( X is open Subset of iff X is open Subset of ) by Def5; :: thesis: verum