let x, y be real number ; :: thesis: ( x in NAT & y in NAT implies x + y in NAT )
reconsider x1 = x, y1 = y as Element of REAL by XREAL_0:def 1;
A1: + x1,y1 = x + y by Lm3;
assume A2: ( x in NAT & y in NAT ) ; :: thesis: x + y in NAT
then ex x9, y9 being Element of REAL+ st
( x1 = x9 & y1 = y9 & + x1,y1 = x9 + y9 ) by ARYTM_0:def 2, ARYTM_2:2;
hence x + y in NAT by A1, A2, ARYTM_2:17; :: thesis: verum