let T be TopSpace; :: thesis: for X being set holds
( X is open Subset of T iff X is open Subset of TopStruct(# the carrier of T,the topology of T #) )
let X be set ; :: thesis: ( X is open Subset of T iff X is open Subset of TopStruct(# the carrier of T,the topology of T #) )
( 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 T iff X is open Subset of TopStruct(# the carrier of T,the topology of T #) ) by Def5; :: thesis: verum