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