let n, n1 be Nat; :: thesis: [n1,(n1 + n)] in addRel (NAT,n)
( n1 in NAT & n1 + n in NAT ) by ORDINAL1:def 12;
hence [n1,(n1 + n)] in addRel (NAT,n) by Th11; :: thesis: verum