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

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