let O be Ordering of F_Rat; :: thesis: O = Positives(F_Rat)
defpred S₁[ Nat] means $1 in O;
A: ( 0. F_Rat = 0 & 1. F_Rat = 1 ) by GAUSSINT:def 14;
B: ( 1. F_Rat in O & 0. F_Rat in O ) by ord3;
IA: S₁[ 0 ] by A, ord3;
E: ( O + O c= O & O * O c= O ) by defpc;

IS: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume C: S₁[k] ; :: thesis: S₁[k + 1]
then consider a being Element of F_Rat such that
D: a = k ;
a + (1. F_Rat) in { (x + y) where x, y is Element of F_Rat : ( x in O & y in O ) } by D, C, B;
then k + 1 in O + O by GAUSSINT:def 14, D, IDEAL_1:def 19;
hence S₁[k + 1] by E; :: thesis: verum

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
Positives(F_Rat) c= O

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in Positives(F_Rat) or o in O )
assume o in Positives(F_Rat) ; :: thesis: o in O
then consider r being Element of RAT such that
A1: ( o = r & 0 <= r ) ;
consider m, n being Integer such that
B1: ( n > 0 & r = m / n ) by RAT_1:1;
reconsider a = n, b = m as Element of F_Rat by RAT_1:def 2, GAUSSINT:def 14;

per cases ( m = 0 or 0 < m or m < 0 ) ;

suppose m = 0 ; :: thesis: o in O

hence o in O by B1, A1, A, ord3; :: thesis: verum

end;

suppose C1: 0 < m ; :: thesis: o in O

0 <= n by B1;
then reconsider n1 = n, m1 = m as Element of NAT by C1, INT_1:3;
C: ( m1 in O & n1 in O ) by I;
not a is zero by B1, GAUSSINT:def 14;
then a " in O by C, ord5;
then b * (a ") in O * O by C;
then b * (a ") in O by E;
hence o in O by A1, B1, GAUSSINT:def 14, GAUSSINT:15; :: thesis: verum

end;

suppose C1: m < 0 ; :: thesis: o in O

then 0 >= n by A1, B1;
then reconsider n1 = - n, m1 = - m as Element of NAT by C1, INT_1:3;
C: ( m1 in O & n1 in O ) by I;
K: - a <> 0. F_Rat by B1, GAUSSINT:def 14;
not - a is zero by B1, GAUSSINT:def 14;
then (- a) " in O by C, ord5;
then F: (- b) * ((- a) ") in O * O by C;
H: - (n ") = - (a ") by B1, GAUSSINT:def 14, GAUSSINT:15;
a <> 0. F_Rat by B1, GAUSSINT:def 14;
then 1. F_Rat = a * (a ") by VECTSP_1:def 10
.= (- (a ")) * (- a) ;
then (- a) " = - (a ") by VECTSP_1:def 10, K;
hence o in O by A1, B1, F, E, H; :: thesis: verum

end;

end;

end;

hence O = Positives(F_Rat) by ordsub; :: thesis: verum