let x, y be Real; :: 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 1, ARYTM_2:2;
hence x + y in NAT by A1, A2, ARYTM_2:16; :: thesis: verum