let X be non empty discrete TopSpace; :: thesis:
let A be Subset of X; :: thesis:

hereby :: thesis:

suppose A is empty ; :: thesis:

hence A is discrete by Th29; :: thesis:

end;

suppose not A is empty ; :: thesis:

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:

end;

end;

end;