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:47;
hence Cl (Down V,B) = (Cl V) /\ B by PRE_TOPC:def 10; :: thesis: verum