hereby :: thesis: ( ( for A being non empty Subset of X holds not A is boundary ) implies X is discrete )

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

end;

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

now :: thesis: for A being Subset of X
for x being Point of X st A = {x} holds
A is open

let A be Subset of X; :: thesis: for x being Point of X st A = {x} holds
A is open
let x be Point of X; :: thesis: ( A = {x} implies A is open )
assume A3: A = {x} ; :: thesis: A is open

hereby :: thesis: verum

per cases ( A = {} or A <> {} ) ;

suppose A = {} ; :: thesis: A is open

hence A is open ; :: thesis: verum

end;

suppose A <> {} ; :: thesis: A is open

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: verum

end;

end;

end;

end;

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