theorem Th23: :: CARDFIL2:50

for p being Element of OrderedNAT holds { x where x is Element of NAT : ex p0 being Element of NAT st
( p = p0 & p0 <= x ) } = uparrow p