let p be Element of OrderedNAT; :: thesis: { x where x is Element of NAT : ex p0 being Element of NAT st
( p = p0 & p0 <= x ) } = uparrow p
reconsider p0 = p as Element of NAT ;
A1: for p being Element of the carrier of OrderedNAT holds { x where x is Element of the carrier of OrderedNAT : p <= x } = uparrow p

proof

let p be Element of OrderedNAT; :: thesis: { x where x is Element of the carrier of OrderedNAT : p <= x } = uparrow p

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: uparrow p c= { x where x is Element of the carrier of OrderedNAT : p <= x }

let t be object ; :: thesis: ( t in { x where x is Element of OrderedNAT : p <= x } implies t in uparrow p )
assume t in { x where x is Element of OrderedNAT : p <= x } ; :: thesis: t in uparrow p
then consider x0 being Element of OrderedNAT such that
A2: t = x0 and
A3: p <= x0 ;
thus t in uparrow p by A2, A3, WAYBEL_0:18; :: thesis: verum

end;

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in uparrow p or t in { x where x is Element of the carrier of OrderedNAT : p <= x } )
assume A4: t in uparrow p ; :: thesis: t in { x where x is Element of the carrier of OrderedNAT : p <= x }
then reconsider t0 = t as Element of OrderedNAT ;
p <= t0 by A4, WAYBEL_0:18;
hence t in { x where x is Element of OrderedNAT : p <= x } ; :: thesis: verum

end;

{ x where x is Element of NAT : ex p0 being Element of NAT st
( p = p0 & p0 <= x ) } = { x where x is Element of OrderedNAT : p <= x } by Lm4;
hence { x where x is Element of NAT : ex p0 being Element of NAT st
( p = p0 & p0 <= x ) } = uparrow p by A1; :: thesis: verum