let GX be TopStruct ; :: thesis: for R, S being Subset of GX st R is closed & S is closed holds
Cl (R /\ S) = (Cl R) /\ (Cl S)
let R, S be Subset of GX; :: thesis: ( R is closed & S is closed implies Cl (R /\ S) = (Cl R) /\ (Cl S) )
assume ( R is closed & S is closed ) ; :: thesis: Cl (R /\ S) = (Cl R) /\ (Cl S)
then A1: ( R = Cl R & S = Cl S ) by PRE_TOPC:52;
A2: Cl (R /\ S) c= (Cl R) /\ (Cl S) by PRE_TOPC:51;
(Cl R) /\ (Cl S) c= Cl (R /\ S) by A1, PRE_TOPC:48;
hence Cl (R /\ S) = (Cl R) /\ (Cl S) by A2, XBOOLE_0:def 10; :: thesis: verum