let X be non empty TopSpace; :: thesis: for A being empty Subset of X holds A is discrete
let A be empty Subset of X; :: thesis: A is discrete
now :: thesis: for D being Subset of X st D c= A holds
ex G being Subset of X st
( G is open & A /\ G = D )
let D be Subset of X; :: thesis: ( D c= A implies ex G being Subset of X st
( G is open & A /\ G = D ) )
assume A1: D c= A ; :: thesis: ex G being Subset of X st
( G is open & A /\ G = D )
now :: thesis: ex G being Element of bool the carrier of X st
( G is open & A /\ G = D )
take G = {} X; :: thesis: ( G is open & A /\ G = D )
thus ( G is open & A /\ G = D ) by A1; :: thesis: verum
end;
hence ex G being Subset of X st
( G is open & A /\ G = D ) ; :: thesis: verum
end;
hence A is discrete ; :: thesis: verum