let GX be non empty TopSpace; :: thesis: for V, B being Subset of GX st V c= B holds

Cl (Down (V,B)) = (Cl V) /\ B

let V, B be Subset of GX; :: thesis: ( V c= B implies Cl (Down (V,B)) = (Cl V) /\ B )

assume V c= B ; :: thesis: Cl (Down (V,B)) = (Cl V) /\ B

then Down (V,B) = V by XBOOLE_1:28;

then Cl (Down (V,B)) = (Cl V) /\ ([#] (GX | B)) by PRE_TOPC:17;

hence Cl (Down (V,B)) = (Cl V) /\ B by PRE_TOPC:def 5; :: thesis: verum

Cl (Down (V,B)) = (Cl V) /\ B

let V, B be Subset of GX; :: thesis: ( V c= B implies Cl (Down (V,B)) = (Cl V) /\ B )

assume V c= B ; :: thesis: Cl (Down (V,B)) = (Cl V) /\ B

then Down (V,B) = V by XBOOLE_1:28;

then Cl (Down (V,B)) = (Cl V) /\ ([#] (GX | B)) by PRE_TOPC:17;

hence Cl (Down (V,B)) = (Cl V) /\ B by PRE_TOPC:def 5; :: thesis: verum