let X0 be SubSpace of X; :: thesis: ( X0 is open & X0 is closed & X0 is discrete )
thus X0 is open by Th15; :: thesis: ( X0 is closed & X0 is discrete )
thus X0 is closed by Th16; :: thesis: X0 is discrete
A1: the topology of X = bool the carrier of X by Def1;
now :: thesis: for S being object st S in bool the carrier of X0 holds
S in the topology of X0
let S be object ; :: 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 :: thesis: ex B being Subset of X st
( B in the topology of X & A = B /\ ([#] X0) )
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 ;
hence the topology of X0 = bool the carrier of X0 ; :: according to TDLAT_3:def 1 :: thesis: verum