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