Cl (Cl P) = Cl P ;
hence Cl P is closed by PRE_TOPC:52; :: thesis: verum