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