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