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] )

proof

let e be object ; :: thesis: ( e in the carrier of N implies ex u being object st
( u in the carrier of N & S₁[e,u] ) )
assume e in the carrier of N ; :: thesis: ex u being object st
( u in the carrier of N & S₁[e,u] )
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: ( u9 in the carrier of N & S₁[e,u9] )
thus u9 in the carrier of N ; :: thesis: S₁[e,u9]
let n, m be Element of N; :: thesis: ( e = n & u9 = m implies n <= m )
assume ( e = n & u9 = m ) ; :: thesis: n <= m
hence n <= m by A2; :: thesis: verum

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: p is greater_or_equal_to_id
let j be Element of N; :: according to WAYBEL28:def 1 :: thesis: j <= p . j
thus j <= p . j by A4; :: thesis: verum