let Y be non empty TopStruct ; :: thesis: for A being Subset of Y st A = the carrier of Y holds
( A is discrete iff Y is discrete )
let A be Subset of Y; :: thesis: ( A = the carrier of Y implies ( A is discrete iff Y is discrete ) )
assume A1: A = the carrier of Y ; :: thesis: ( A is discrete iff Y is discrete )
hereby :: thesis: ( Y is discrete implies A is discrete )
assume A2: A is discrete ; :: thesis: Y is discrete
now :: thesis: for C being object st C in bool the carrier of Y holds
C in the topology of Y
let C be object ; :: thesis: ( C in bool the carrier of Y implies C in the topology of Y )
assume C in bool the carrier of Y ; :: thesis: C in the topology of Y
then reconsider B = C as Subset of Y ;
consider G being Subset of Y such that
A3: G is open and
A4: A /\ G = B by A1, A2;
G = B by A1, A4, XBOOLE_1:28;
hence C in the topology of Y by A3; :: thesis: verum
end;
then bool the carrier of Y c= the topology of Y by TARSKI:def 3;
then the topology of Y = bool the carrier of Y ;
hence Y is discrete by TDLAT_3:def 1; :: thesis: verum
end;
hereby :: thesis: verum
assume Y is discrete ; :: thesis: A is discrete
then reconsider Y = Y as non empty discrete TopStruct ;
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 A5: D c= A ; :: thesis: ex G being Subset of Y st
( G is open & A /\ G = D )
reconsider G = D as Subset of Y ;
take G = G; :: thesis: ( G is open & A /\ G = D )
thus G is open by TDLAT_3:15; :: thesis: A /\ G = D
thus A /\ G = D by A5, XBOOLE_1:28; :: thesis: verum
end;
hence A is discrete ; :: thesis: verum
end;