hereby :: thesis:

assume A1: X is discrete ; :: thesis:
let A be non empty Subset of X; :: thesis:
assume A is boundary ; :: thesis:
then Int A <> A ;
then not A is open by TOPS_1:23;
hence contradiction by A1; :: thesis:

end;

assume A2: for A being non empty Subset of X holds not A is boundary ; :: thesis:

now :: thesis:

let A be Subset of X; :: thesis:
let x be Point of X; :: thesis:
assume A3: A = {x} ; :: thesis:

hereby :: thesis:

per cases ;

suppose A = {} ; :: thesis:

hence A is open ; :: thesis:

end;

suppose A <> {} ; :: thesis:

then not A is boundary by A2;
then A4: Int A <> {} by TOPS_1:48;
Int A c= {x} by A3, TOPS_1:16;
hence A is open by A3, A4, ZFMISC_1:33; :: thesis:

end;

end;

end;

end;

hence X is discrete by TDLAT_3:17; :: thesis: