defpred S₁[ object , object ] means for n, m being Element of N st N = n & c₂ = m holds
n <= m;
A1: for e being object st e in the carrier of N holds
ex u being object st
( u in the carrier of N & S₁[e,u] )

let e be object ; :: thesis:
assume e in the carrier of N ; :: thesis:
then reconsider e9 = e as Element of N ;
consider u9 being Element of N such that
A2: e9 <= u9 and
e9 <= u9 by Th5;
take u9 ; :: thesis:
thus u9 in the carrier of N ; :: thesis:
let n, m be Element of N; :: thesis:
assume ( e = n & u9 = m ) ; :: thesis:
hence n <= m by A2; :: thesis:

end;

consider p being Function such that
A3: ( dom p = the carrier of N & rng p c= the carrier of N ) and
A4: for e being object st e in the carrier of N holds
S₁[e,p . e] from FUNCT_1:sch 6(A1);
reconsider p = p as Function of N,N by A3, FUNCT_2:2;
take p ; :: thesis:
let j be Element of N; :: according to WAYBEL28:def 1 :: thesis:
thus j <= p . j by A4; :: thesis: