let X be TopSpace; :: thesis: for X1, X2 being TopSpace st X2 = TopStruct(# the carrier of X1, the topology of X1 #) holds
( X1 is closed SubSpace of X iff X2 is closed SubSpace of X )

let X1, X2 be TopSpace; :: thesis: ( X2 = TopStruct(# the carrier of X1, the topology of X1 #) implies ( X1 is closed SubSpace of X iff X2 is closed SubSpace of X ) )
assume A1: X2 = TopStruct(# the carrier of X1, the topology of X1 #) ; :: thesis: ( X1 is closed SubSpace of X iff X2 is closed SubSpace of X )
thus ( X1 is closed SubSpace of X implies X2 is closed SubSpace of X ) :: thesis: ( X2 is closed SubSpace of X implies X1 is closed SubSpace of X )
proof
assume A2: X1 is closed SubSpace of X ; :: thesis: X2 is closed SubSpace of X
then reconsider Y2 = X2 as SubSpace of X by ;
reconsider A2 = the carrier of Y2 as Subset of X by TSEP_1:1;
A2 is closed by ;
hence X2 is closed SubSpace of X by TSEP_1:11; :: thesis: verum
end;
assume A3: X2 is closed SubSpace of X ; :: thesis: X1 is closed SubSpace of X
then reconsider Y1 = X1 as SubSpace of X by ;
reconsider A1 = the carrier of Y1 as Subset of X by TSEP_1:1;
A1 is closed by ;
hence X1 is closed SubSpace of X by TSEP_1:11; :: thesis: verum