defpred S1[ object , object ] means for n, m being Element of N st N = n & c2 = 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 & S1[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 & S1[e,u] ) )

assume e in the carrier of N ; :: thesis: ex u being object st
( u in the carrier of N & S1[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 & S1[e,u9] )
thus u9 in the carrier of N ; :: thesis: S1[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
S1[e,p . e] from reconsider p = p as Function of N,N by ;
take p ; :: thesis:
let j be Element of N; :: according to WAYBEL28:def 1 :: thesis: j <= p . j
thus j <= p . j by A4; :: thesis: verum