Positives(F_Rat) is positive_cone ;
hence F_Rat is ordered ; :: thesis: verum