let N be non empty directed RelStr ; :: thesis: ex p being Function of N,N st p is greater_or_equal_to_id
defpred S₁[ set , set ] means for n, m being Element of N st $1 = n & $2 = m holds
n <= m;
A1: for e being set st e in the carrier of N holds
ex u being set st
( u in the carrier of N & S₁[e,u] )

proof

let e be set ; :: thesis: ( e in the carrier of N implies ex u being set st
( u in the carrier of N & S₁[e,u] ) )
assume e in the carrier of N ; :: thesis: ex u being set 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 set st e in the carrier of N holds
S₁[e,p . e] from WELLORD2:sch 1(A1);
reconsider p = p as Function of N,N by A3, FUNCT_2:4;
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