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

Cl (Down (V,B)) c= Cl V

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

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

then Cl (Down (V,B)) = (Cl V) /\ B by Th29;

hence Cl (Down (V,B)) c= Cl V by XBOOLE_1:17; :: thesis: verum

Cl (Down (V,B)) c= Cl V

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

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

then Cl (Down (V,B)) = (Cl V) /\ B by Th29;

hence Cl (Down (V,B)) c= Cl V by XBOOLE_1:17; :: thesis: verum