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