B: now :: thesis: for o being object st o in Positives(INT.Ring) holds
o in Positives(F_Rat) /\ the carrier of INT.Ring
let o be object ; :: thesis: ( o in Positives(INT.Ring) implies o in Positives(F_Rat) /\ the carrier of INT.Ring )
assume o in Positives(INT.Ring) ; :: thesis: o in Positives(F_Rat) /\ the carrier of INT.Ring
then consider i being Element of INT such that
A1: ( o = i & 0 <= i ) ;
reconsider r = i as Element of RAT by RAT_1:def 2;
r in { x where x is Element of RAT : 0 <= x } by A1;
hence o in Positives(F_Rat) /\ the carrier of INT.Ring by A1, INT_3:def 3, XBOOLE_0:def 4; :: thesis: verum
end;
now :: thesis: for o being object st o in Positives(F_Rat) /\ the carrier of INT.Ring holds
o in Positives(INT.Ring)
let o be object ; :: thesis: ( o in Positives(F_Rat) /\ the carrier of INT.Ring implies o in Positives(INT.Ring) )
assume B1: o in Positives(F_Rat) /\ the carrier of INT.Ring ; :: thesis: o in Positives(INT.Ring)
then ( o in Positives(F_Rat) & o in the carrier of INT.Ring ) by XBOOLE_0:def 4;
then consider a being Element of RAT such that
B2: ( o = a & 0 <= a ) ;
a is Element of INT by B1, B2, INT_3:def 3, XBOOLE_0:def 4;
hence o in Positives(INT.Ring) by B2; :: thesis: verum
end;
then Positives(INT.Ring) is positive_cone by RING_3:47, B, lemsubord, TARSKI:2;
hence ( Positives(INT.Ring) is add-closed & Positives(INT.Ring) is mult-closed & Positives(INT.Ring) is negative-disjoint & Positives(INT.Ring) is spanning ) ; :: thesis: verum