let O be Ordering of INT.Ring; :: thesis: O = Positives(INT.Ring)
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: 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 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: verum

end;

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

now :: thesis: for o being object st o in Positives(INT.Ring) holds
o in O

let o be object ; :: thesis: ( o in Positives(INT.Ring) implies o in O )
assume o in Positives(INT.Ring) ; :: thesis: o in O
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: verum

end;

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