Positives(INT.Ring) is positive_cone ;
hence INT.Ring is ordered ; :: thesis: verum