Positives(F_Real) is positive_cone by lemEX;
hence ( Positives(F_Real) is add-closed & Positives(F_Real) is mult-closed & Positives(F_Real) is negative-disjoint & Positives(F_Real) is spanning ) ; :: thesis: verum