let X be non empty discrete TopSpace; :: thesis: for A being Subset of X holds A is discrete
let A be Subset of X; :: thesis: A is discrete

hereby :: thesis: verum

per cases ( A is empty or not A is empty ) ;

suppose A is empty ; :: thesis: A is discrete

hence A is discrete by Th29; :: thesis: verum

end;

suppose not A is empty ; :: thesis: A is discrete

then ex X0 being non empty strict SubSpace of X st A = the carrier of X0 by TSEP_1:10;
hence A is discrete by Th20; :: thesis: verum

end;

end;

end;