set S = Positives(F_Rat) ;
set R = F_Rat ;
A: Positives(F_Rat) + Positives(F_Rat) c= Positives(F_Rat)

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in Positives(F_Rat) + Positives(F_Rat) or o in Positives(F_Rat) )
assume o in Positives(F_Rat) + Positives(F_Rat) ; :: thesis: o in Positives(F_Rat)
then o in { (a + b) where a, b is Element of F_Rat : ( a in Positives(F_Rat) & b in Positives(F_Rat) ) } by IDEAL_1:def 19;
then consider a, b being Element of F_Rat such that
A: ( o = a + b & a in Positives(F_Rat) & b in Positives(F_Rat) ) ;
consider x being Element of RAT such that
B: ( x = a & 0 <= x ) by A;
consider y being Element of RAT such that
C: ( y = b & 0 <= y ) by A;
thus o in Positives(F_Rat) by A, B, C, GAUSSINT:def 14; :: thesis: verum

end;

B: Positives(F_Rat) * Positives(F_Rat) c= Positives(F_Rat)

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in Positives(F_Rat) * Positives(F_Rat) or o in Positives(F_Rat) )
assume o in Positives(F_Rat) * Positives(F_Rat) ; :: thesis: o in Positives(F_Rat)
then consider a, b being Element of F_Rat such that
A: ( o = a * b & a in Positives(F_Rat) & b in Positives(F_Rat) ) ;
consider x being Element of RAT such that
B: ( x = a & 0 <= x ) by A;
consider y being Element of RAT such that
C: ( y = b & 0 <= y ) by A;
thus o in Positives(F_Rat) by A, B, C, GAUSSINT:def 14; :: thesis: verum

end;

K: now :: thesis: for o being object st o in Positives(F_Rat) /\ (- Positives(F_Rat)) holds
o in {(0. F_Rat)}

let o be object ; :: thesis: ( o in Positives(F_Rat) /\ (- Positives(F_Rat)) implies o in {(0. F_Rat)} )
assume K0: o in Positives(F_Rat) /\ (- Positives(F_Rat)) ; :: thesis: o in {(0. F_Rat)}
then K1: ( o in Positives(F_Rat) & o in - Positives(F_Rat) ) by XBOOLE_0:def 4;
reconsider x = o as Element of F_Rat by K0;
consider y1 being Element of RAT such that
K2: ( y1 = o & 0 <= y1 ) by K1;
consider y2 being Element of F_Rat such that
K3: ( - y2 = o & y2 in Positives(F_Rat) ) by K1;
reconsider y2 = y2 as Element of RAT by GAUSSINT:def 14;
consider y being Element of RAT such that
K4: ( y2 = y & 0 <= y ) by K3;
y1 = 0. F_Rat by K4, K2, K3, GAUSSINT:def 14;
hence o in {(0. F_Rat)} by K2, TARSKI:def 1; :: thesis: verum

end;

C: now :: thesis: for o being object st o in {(0. F_Rat)} holds
o in Positives(F_Rat) /\ (- Positives(F_Rat))

let o be object ; :: thesis: ( o in {(0. F_Rat)} implies o in Positives(F_Rat) /\ (- Positives(F_Rat)) )
assume K0: o in {(0. F_Rat)} ; :: thesis: o in Positives(F_Rat) /\ (- Positives(F_Rat))
then K1: o = 0. F_Rat by TARSKI:def 1;
reconsider x = o as Element of RAT by K0, GAUSSINT:def 14;
reconsider xx = x as Element of F_Rat by GAUSSINT:def 14;
K3: x in Positives(F_Rat) by K0, GAUSSINT:def 14;
- xx in { (- s) where s is Element of F_Rat : s in Positives(F_Rat) } by K3;
hence o in Positives(F_Rat) /\ (- Positives(F_Rat)) by K1, K3, XBOOLE_0:def 4; :: thesis: verum

end;

F: now :: thesis: for o being object st o in the carrier of F_Rat holds
o in Positives(F_Rat) \/ (- Positives(F_Rat))

let o be object ; :: thesis: ( o in the carrier of F_Rat implies b₁ in Positives(F_Rat) \/ (- Positives(F_Rat)) )
assume o in the carrier of F_Rat ; :: thesis: b₁ in Positives(F_Rat) \/ (- Positives(F_Rat))
then reconsider x = o as Element of RAT by GAUSSINT:def 14;
F1: - x is Element of RAT by RAT_1:def 2;
reconsider xx = x as Element of F_Rat by GAUSSINT:def 14;

per cases ( 0 <= x or 0 <= - x ) ;

suppose 0 <= x ; :: thesis: b₁ in Positives(F_Rat) \/ (- Positives(F_Rat))

then x in Positives(F_Rat) ;
hence o in Positives(F_Rat) \/ (- Positives(F_Rat)) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose 0 <= - x ; :: thesis: b₁ in Positives(F_Rat) \/ (- Positives(F_Rat))

then - xx in Positives(F_Rat) by F1;
then - (- xx) in - Positives(F_Rat) ;
hence o in Positives(F_Rat) \/ (- Positives(F_Rat)) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

for o being object st o in Positives(F_Rat) \/ (- Positives(F_Rat)) holds
o in the carrier of F_Rat ;
then Positives(F_Rat) is positive_cone by A, B, C, K, F, TARSKI:2;
hence ( Positives(F_Rat) is add-closed & Positives(F_Rat) is mult-closed & Positives(F_Rat) is negative-disjoint & Positives(F_Rat) is spanning ) ; :: thesis: verum