let m, n be Nat; :: thesis: for no being Element of OrderedNAT st n = no & m in uparrow no holds
n <= m
let no be Element of OrderedNAT; :: thesis: ( n = no & m in uparrow no implies n <= m )
assume that
A1: n = no and
A2: m in uparrow no ; :: thesis: n <= m
m in { x where x is Element of NAT : ex p0 being Element of NAT st
( no = p0 & p0 <= x ) } by A2, CARDFIL2:50;
then ex x being Element of NAT st
( m = x & ex p0 being Element of NAT st
( no = p0 & p0 <= x ) ) ;
hence n <= m by A1; :: thesis: verum