let TS be TopSpace; :: thesis: for P, Q being Subset of TS st P is dense & Q is dense & Q is open holds
P /\ Q is dense
let P, Q be Subset of TS; :: thesis: ( P is dense & Q is dense & Q is open implies P /\ Q is dense )
assume that
A1: P is dense and
A2: Cl Q = [#] TS and
A3: Q is open ; :: according to TOPS_1:def 3 :: thesis: P /\ Q is dense
thus Cl (P /\ Q) = [#] TS by A1, A2, A3, Th81; :: according to TOPS_1:def 3 :: thesis: verum