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