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 in the topology of T iff ([#] TopStruct(# the carrier of T,the topology of T #)) \ X in the topology of TopStruct(# the carrier of T,the topology of T #) ) ;
then ( ([#] T) \ X is open iff ([#] TopStruct(# the carrier of T,the topology of T #)) \ X is open ) by Def5;
hence ( X is closed Subset of T iff X is closed Subset of TopStruct(# the carrier of T,the topology of T #) ) by Def6; :: thesis: verum