let TS be TopSpace; :: thesis: for P, Q being Subset of TS st P is nowhere_dense & Q is nowhere_dense holds
P \/ Q is nowhere_dense
let P, Q be Subset of TS; :: thesis: ( P is nowhere_dense & Q is nowhere_dense implies P \/ Q is nowhere_dense )
assume that
A1: P is nowhere_dense and
A2: Q is nowhere_dense ; :: thesis: P \/ Q is nowhere_dense
A3: Cl Q is boundary by A2;
Cl P is boundary by A1;
then (Cl P) \/ (Cl Q) is boundary by A3, Th49;
then Cl (P \/ Q) is boundary by PRE_TOPC:20;
hence P \/ Q is nowhere_dense ; :: thesis: verum