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

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