let TS be TopSpace; :: thesis: for Q, K being Subset of TS st Q is open holds
Q /\ (Cl K) c= Cl (Q /\ K)
let Q, K be Subset of TS; :: thesis: ( Q is open implies Q /\ (Cl K) c= Cl (Q /\ K) )
assume A1: Q is open ; :: thesis: Q /\ (Cl K) c= Cl (Q /\ K)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q /\ (Cl K) or x in Cl (Q /\ K) )
assume A2: x in Q /\ (Cl K) ; :: thesis: x in Cl (Q /\ K)
then A3: x in Cl K by XBOOLE_0:def 4;
reconsider p99 = x as Point of TS by A2;
A4: not TS is empty by A2;
A5: x in Q by A2, XBOOLE_0:def 4;
for Q1 being Subset of TS st Q1 is open & p99 in Q1 holds
Q /\ K meets Q1
proof
let Q1 be Subset of TS; :: thesis: ( Q1 is open & p99 in Q1 implies Q /\ K meets Q1 )
assume A6: Q1 is open ; :: thesis: ( not p99 in Q1 or Q /\ K meets Q1 )
assume p99 in Q1 ; :: thesis: Q /\ K meets Q1
then p99 in Q1 /\ Q by A5, XBOOLE_0:def 4;
then K meets Q1 /\ Q by A1, A3, A4, A6, Th12;
then A7: K /\ (Q1 /\ Q) <> {} ;
K /\ (Q1 /\ Q) = (Q /\ K) /\ Q1 by XBOOLE_1:16;
hence Q /\ K meets Q1 by A7; :: thesis: verum
end;
hence x in Cl (Q /\ K) by A4, Th12; :: thesis: verum