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 ) } = { 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 : ex p0 being Element of NAT st
( p = p0 & p0 <= x ) }
let t be object ; :: thesis: ( t in { x where x is Element of NAT : ex p0 being Element of NAT st
( p = p0 & p0 <= x ) } implies t in { x where x is Element of OrderedNAT : p <= x } )
assume t in { x where x is Element of NAT : ex p0 being Element of NAT st
( p = p0 & p0 <= x ) } ; :: thesis: t in { x where x is Element of OrderedNAT : p <= x }
then consider x0 being Element of NAT such that
A1: t = x0 and
A2: ex p0 being Element of NAT st
( p = p0 & p0 <= x0 ) ;
consider p0 being Element of NAT such that
A3: p = p0 and
A4: p0 <= x0 by A2;
reconsider x1 = x0 as Element of OrderedNAT ;
p <= x1 by A4, A3;
hence t in { x where x is Element of OrderedNAT : p <= x } by A1; :: 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 : ex p0 being Element of NAT st
( p = p0 & p0 <= x ) } )
assume t in { x where x is Element of OrderedNAT : p <= x } ; :: thesis: t in { x where x is Element of NAT : ex p0 being Element of NAT st
( p = p0 & p0 <= x ) }
then consider x0 being Element of OrderedNAT such that
A5: t = x0 and
A6: p <= x0 ;
reconsider p0 = p as Element of NAT ;
consider a, b being Element of NAT such that
A7: [p0,x0] = [a,b] and
A8: a <= b by A6;
( p0 = a & x0 = b ) by A7, XTUPLE_0:1;
hence t in { x where x is Element of NAT : ex p0 being Element of NAT st
( p = p0 & p0 <= x ) } by A5, A8; :: thesis: verum