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 that
A1: R is closed and
A2: S is closed ; :: thesis: Cl (R /\ S) = (Cl R) /\ (Cl S)
A3: S = Cl S by A2, PRE_TOPC:22;
A4: Cl (R /\ S) c= (Cl R) /\ (Cl S) by PRE_TOPC:21;
R = Cl R by A1, PRE_TOPC:22;
then (Cl R) /\ (Cl S) c= Cl (R /\ S) by A3, PRE_TOPC:18;
hence Cl (R /\ S) = (Cl R) /\ (Cl S) by A4; :: thesis: verum