let TS be TopSpace; :: thesis: for Q, K being Subset of TS st Q is open holds
Cl (Q /\ (Cl K)) = Cl (Q /\ K)
let Q, K be Subset of TS; :: thesis: ( Q is open implies Cl (Q /\ (Cl K)) = Cl (Q /\ K) )
A1: Cl (Q /\ K) c= Cl (Q /\ (Cl K))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Cl (Q /\ K) or x in Cl (Q /\ (Cl K)) )
assume A2: x in Cl (Q /\ K) ; :: thesis: x in Cl (Q /\ (Cl K))
then reconsider p99 = x as Point of TS ;
A3: not TS is empty by A2;
for Q1 being Subset of TS st Q1 is open & p99 in Q1 holds
Q /\ (Cl K) meets Q1

proof

let Q1 be Subset of TS; :: thesis: ( Q1 is open & p99 in Q1 implies Q /\ (Cl K) meets Q1 )
assume A4: Q1 is open ; :: thesis: ( not p99 in Q1 or Q /\ (Cl K) meets Q1 )
assume p99 in Q1 ; :: thesis: Q /\ (Cl K) meets Q1
then Q /\ K meets Q1 by A2, A3, A4, Th12;
then A5: (Q /\ K) /\ Q1 <> {} ;
Q /\ K c= Q /\ (Cl K) by PRE_TOPC:18, XBOOLE_1:26;
then (Q /\ (Cl K)) /\ Q1 <> {} by A5, XBOOLE_1:3, XBOOLE_1:26;
hence Q /\ (Cl K) meets Q1 ; :: thesis: verum

end;

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

end;

assume Q is open ; :: thesis: Cl (Q /\ (Cl K)) = Cl (Q /\ K)
then Cl (Q /\ (Cl K)) c= Cl (Cl (Q /\ K)) by Th13, PRE_TOPC:19;
hence Cl (Q /\ (Cl K)) = Cl (Q /\ K) by A1; :: thesis: verum