let Y be non empty TopStruct ; :: thesis: for Y0 being non empty SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 holds
( A is discrete iff Y0 is discrete )
let Y0 be non empty SubSpace of Y; :: thesis: for A being Subset of Y st A = the carrier of Y0 holds
( A is discrete iff Y0 is discrete )
let A be Subset of Y; :: thesis: ( A = the carrier of Y0 implies ( A is discrete iff Y0 is discrete ) )
assume A1: A = the carrier of Y0 ; :: thesis: ( A is discrete iff Y0 is discrete )
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: ( Y0 is discrete implies A is discrete )

assume A4: A is discrete ; :: thesis: Y0 is discrete

now :: thesis: for C being object st C in bool the carrier of Y0 holds
C in the topology of Y0

let C be object ; :: thesis: ( C in bool the carrier of Y0 implies C in the topology of Y0 )
assume C in bool the carrier of Y0 ; :: thesis: C in the topology of Y0
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: verum

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: verum

end;

hereby :: thesis: verum

assume A7: Y0 is discrete ; :: thesis: A is discrete

now :: thesis: for D being Subset of Y st D c= A holds
ex G being Subset of Y st
( G is open & A /\ G = D )

let D be Subset of Y; :: thesis: ( D c= A implies ex G being Subset of Y st
( G is open & A /\ G = D ) )
assume D c= A ; :: thesis: ex G being Subset of Y st
( G is open & A /\ G = D )
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: ( G is open & A /\ G = D )
thus G is open by A8; :: thesis: A /\ G = D
thus A /\ G = D by A1, A9; :: thesis: verum

end;

hence A is discrete ; :: thesis: verum

end;