let X be non empty TopSpace; :: thesis: for A being Subset of X st A is open & A is dense holds
A is everywhere_dense
let A be Subset of X; :: thesis: ( A is open & A is dense implies A is everywhere_dense )
assume A is open ; :: thesis: ( not A is dense or A is everywhere_dense )
then A1: A = Int A by TOPS_1:23;
assume A is dense ; :: thesis: A is everywhere_dense
hence A is everywhere_dense by A1, Th35; :: thesis: verum