let m, n be Nat; :: thesis: for no being Element of OrderedNAT st n = no & n <= m holds

m in uparrow no

let no be Element of OrderedNAT; :: thesis: ( n = no & n <= m implies m in uparrow no )

assume that

A1: no = n and

A2: n <= m ; :: thesis: m in uparrow no

reconsider m = m as Element of NAT by ORDINAL1:def 12;

reconsider p0 = no as Element of NAT ;

m in { x where x is Element of NAT : ex p0 being Element of NAT st

( no = p0 & p0 <= x ) } by A1, A2;

hence m in uparrow no by CARDFIL2:50; :: thesis: verum

m in uparrow no

let no be Element of OrderedNAT; :: thesis: ( n = no & n <= m implies m in uparrow no )

assume that

A1: no = n and

A2: n <= m ; :: thesis: m in uparrow no

reconsider m = m as Element of NAT by ORDINAL1:def 12;

reconsider p0 = no as Element of NAT ;

m in { x where x is Element of NAT : ex p0 being Element of NAT st

( no = p0 & p0 <= x ) } by A1, A2;

hence m in uparrow no by CARDFIL2:50; :: thesis: verum