let TS be TopSpace; :: thesis: for P being Subset of TS st P is open & P is nowhere_dense holds
P = {}
let P be Subset of TS; :: thesis: ( P is open & P is nowhere_dense implies P = {} )
assume that
A1: P is open and
A2: P is nowhere_dense and
A3: P <> {} ; :: thesis: contradiction
P meets P ` by A1, A2, A3, Th45;
hence contradiction by XBOOLE_1:79; :: thesis: verum