let A be Subset of TS; :: thesis: ( A is empty implies A is nowhere_dense )
assume A1: A is empty ; :: thesis: A is nowhere_dense
(Cl ({} TS)) ` = ({} TS) ` by PRE_TOPC:52
.= [#] TS ;
hence (Cl A) ` is dense by A1; :: according to TOPS_1:def 4,TOPS_1:def 5 :: thesis: verum