let Y be non empty TopStruct ; :: thesis:
let Y0 be non empty SubSpace of Y; :: thesis:
let A be Subset of Y; :: thesis:
assume A1: A = the carrier of Y0 ; :: thesis:
A2: [#] Y = the carrier of Y ;
[#] Y0 = the carrier of Y0 ;
then A3: the carrier of Y0 c= the carrier of Y by A2, PRE_TOPC:def 4;

hereby :: thesis:

assume A4: A is discrete ; :: thesis:

now :: thesis:

let C be object ; :: thesis:
assume C in bool the carrier of Y0 ; :: thesis:
then reconsider B = C as Subset of Y0 ;
reconsider D = B as Subset of Y by A3, XBOOLE_1:1;
consider G being Subset of Y such that
A5: G is open and
A6: A /\ G = D by A1, A4;
( G in the topology of Y & B = G /\ ([#] Y0) ) by A1, A6, A5;
hence C in the topology of Y0 by PRE_TOPC:def 4; :: thesis:

end;

then bool the carrier of Y0 c= the topology of Y0 by TARSKI:def 3;
then the topology of Y0 = bool the carrier of Y0 ;
hence Y0 is discrete by TDLAT_3:def 1; :: thesis:

end;

hereby :: thesis:

assume A7: Y0 is discrete ; :: thesis:

now :: thesis:

let D be Subset of Y; :: thesis:
assume D c= A ; :: thesis:
then reconsider B = D as Subset of Y0 by A1;
B is open by A7, TDLAT_3:15;
then B in the topology of Y0 ;
then consider G being Subset of Y such that
A8: G in the topology of Y and
A9: B = G /\ ([#] Y0) by PRE_TOPC:def 4;
reconsider G = G as Subset of Y ;
take G = G; :: thesis:
thus G is open by A8; :: thesis:
thus A /\ G = D by A1, A9; :: thesis:

end;

hence A is discrete ; :: thesis:

end;