let O be Ordering of INT.Ring; :: thesis:
defpred S₁[ Nat] means $1 in O;
B: ( 1. INT.Ring in O & 0. INT.Ring in O ) by ord3;
( 0. INT.Ring = 0 & 1. INT.Ring = 1 ) by INT_3:def 3;
then IA: S₁[ 0 ] by ord3;
E: O + O c= O by defpc;

IS: now :: thesis:

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

end;

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

now :: thesis:

let o be object ; :: thesis:
assume o in Positives(INT.Ring) ; :: thesis:
then consider i being Element of INT such that
A: ( o = i & 0 <= i ) ;
i is Element of NAT by A, INT_1:3;
hence o in O by A, I; :: thesis:

end;

then Positives(INT.Ring) c= O ;
hence O = Positives(INT.Ring) by ordsub; :: thesis: