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

assume A1: X is almost_discrete ; :: thesis: for A being non empty Subset of X holds not A is nowhere_dense
let A be non empty Subset of X; :: thesis: not A is nowhere_dense
Cl A is open by A1, TDLAT_3:22;
then Cl A = Int (Cl A) by TOPS_1:23;
then Int (Cl A) <> {} by PRE_TOPC:18, XBOOLE_1:3;
hence not A is nowhere_dense by TOPS_3:def 3; :: thesis: verum

end;

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

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

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

hereby :: thesis: verum

Fr (Cl A) = {} by A2;
then (Cl A) \ (Int (Cl A)) = {} by TOPS_1:43;
then A3: Cl A c= Int (Cl A) by XBOOLE_1:37;
Int (Cl A) c= Cl A by TOPS_1:16;
hence Cl A is open by A3, XBOOLE_0:def 10; :: thesis: verum

end;

end;

hence X is almost_discrete by TDLAT_3:25; :: thesis: verum