let X be non empty TopSpace; :: thesis: for A, B being Subset of X st A is dense & B is nowhere_dense holds
A \ B is dense
let A, B be Subset of X; :: thesis: ( A is dense & B is nowhere_dense implies A \ B is dense )
assume A1: A is dense ; :: thesis: ( not B is nowhere_dense or A \ B is dense )
A2: A \ B = (B `) /\ A by SUBSET_1:13;
assume B is nowhere_dense ; :: thesis: A \ B is dense
then B ` is everywhere_dense by Th40;
hence A \ B is dense by A1, A2, Th45; :: thesis: verum