let TS be TopSpace; :: thesis: for P being Subset of TS st P is dense holds
for Q being Subset of TS st Q is open holds
Cl Q = Cl (Q /\ P)
let P be Subset of TS; :: thesis: ( P is dense implies for Q being Subset of TS st Q is open holds
Cl Q = Cl (Q /\ P) )
assume A1: P is dense ; :: thesis: for Q being Subset of TS st Q is open holds
Cl Q = Cl (Q /\ P)
let Q be Subset of TS; :: thesis: ( Q is open implies Cl Q = Cl (Q /\ P) )
assume A2: Q is open ; :: thesis: Cl Q = Cl (Q /\ P)
thus Cl Q c= Cl (Q /\ P) :: according to XBOOLE_0:def 10 :: thesis: Cl (Q /\ P) c= Cl Q

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Cl Q or x in Cl (Q /\ P) )
assume A3: x in Cl Q ; :: thesis: x in Cl (Q /\ P)
then A4: not TS is empty ;

now :: thesis: for Q1 being Subset of TS st Q1 is open & x in Q1 holds
Q /\ P meets Q1

let Q1 be Subset of TS; :: thesis: ( Q1 is open & x in Q1 implies Q /\ P meets Q1 )
assume A5: Q1 is open ; :: thesis: ( x in Q1 implies Q /\ P meets Q1 )
assume x in Q1 ; :: thesis: Q /\ P meets Q1
then Q meets Q1 by A3, A4, A5, Th12;
then Q /\ Q1 <> {} ;
then P meets Q /\ Q1 by A1, A2, A5, Th45;
then A6: P /\ (Q /\ Q1) <> {} ;
P /\ (Q /\ Q1) = (Q /\ P) /\ Q1 by XBOOLE_1:16;
hence Q /\ P meets Q1 by A6; :: thesis: verum

end;

hence x in Cl (Q /\ P) by A3, A4, Th12; :: thesis: verum

end;

thus Cl (Q /\ P) c= Cl Q by PRE_TOPC:19, XBOOLE_1:17; :: thesis: verum