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