let X0 be SubSpace of X; :: thesis: ( X0 is open & X0 is closed & X0 is discrete )
thus X0 is open :: thesis: ( X0 is closed & X0 is discrete )

proof

let A be Subset of X; :: according to TSEP_1:def 1 :: thesis: ( not A = the carrier of X0 or A is open )
thus ( not A = the carrier of X0 or A is open ) by Th17; :: thesis: verum

end;

thus X0 is closed :: thesis: X0 is discrete

proof

let A be Subset of X; :: according to BORSUK_1:def 11 :: thesis: ( not A = the carrier of X0 or A is closed )
thus ( not A = the carrier of X0 or A is closed ) by Th18; :: thesis: verum

end;

A1: the topology of X = bool the carrier of X by Def1;

now

let S be set ; :: thesis: ( S in bool the carrier of X0 implies S in the topology of X0 )
assume S in bool the carrier of X0 ; :: thesis: S in the topology of X0
then reconsider A = S as Subset of X0 ;
the carrier of X0 c= the carrier of X by BORSUK_1:1;
then reconsider B = A as Subset of X by XBOOLE_1:1;

now

take B = B; :: thesis: ( B in the topology of X & A = B /\ ([#] X0) )
thus ( B in the topology of X & A = B /\ ([#] X0) ) by A1, XBOOLE_1:28; :: thesis: verum

end;

hence S in the topology of X0 by PRE_TOPC:def 4; :: thesis: verum

end;

then bool the carrier of X0 c= the topology of X0 by TARSKI:def 3;
hence the topology of X0 = bool the carrier of X0 by XBOOLE_0:def 10; :: according to TDLAT_3:def 1 :: thesis: verum