let p be Element of OrderedNAT; :: thesis: for p0 being Element of NAT st p = p0 holds
{ x where x is Element of NAT : p0 <= x } = { x where x is Element of OrderedNAT : p <= x }
let p0 be Element of NAT ; :: thesis: ( p = p0 implies { x where x is Element of NAT : p0 <= x } = { x where x is Element of OrderedNAT : p <= x } )
assume A1: p = p0 ; :: thesis: { x where x is Element of NAT : p0 <= x } = { x where x is Element of OrderedNAT : p <= x }

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

let t be object ; :: thesis: ( t in { x where x is Element of NAT : p0 <= x } implies t in { x where x is Element of OrderedNAT : p <= x } )
assume t in { x where x is Element of NAT : p0 <= x } ; :: thesis: t in { x where x is Element of OrderedNAT : p <= x }
then consider x0 being Element of NAT such that
A2: t = x0 and
A3: p0 <= x0 ;
reconsider x1 = x0 as Element of OrderedNAT ;
p <= x1 by A3, A1;
hence t in { x where x is Element of OrderedNAT : p <= x } by A2; :: thesis: verum

end;

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { x where x is Element of OrderedNAT : p <= x } or t in { x where x is Element of NAT : p0 <= x } )
assume t in { x where x is Element of OrderedNAT : p <= x } ; :: thesis: t in { x where x is Element of NAT : p0 <= x }
then consider x0 being Element of OrderedNAT such that
A4: t = x0 and
A5: p <= x0 ;
consider a, b being Element of NAT such that
A6: [p0,x0] = [a,b] and
A7: a <= b by A1, A5;
( p0 = a & x0 = b ) by A6, XTUPLE_0:1;
hence t in { x where x is Element of NAT : p0 <= x } by A4, A7; :: thesis: verum