defpred S_{1}[ object , object ] means for n, m being Element of N st N = n & c_{2} = 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_{1}[e,u] )

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_{1}[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

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

proof

consider p being Function such that
let e be object ; :: thesis: ( e in the carrier of N implies ex u being object st

( u in the carrier of N & S_{1}[e,u] ) )

assume e in the carrier of N ; :: thesis: ex u being object st

( u in the carrier of N & S_{1}[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_{1}[e,u9] )

thus u9 in the carrier of N ; :: thesis: S_{1}[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;( u in the carrier of N & S

assume e in the carrier of N ; :: thesis: ex u being object st

( u in the carrier of N & S

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

thus u9 in the carrier of N ; :: thesis: S

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

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

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