let n1, n2 be Nat; :: thesis: (addRel (NAT,n1)) * (addRel (NAT,n2)) = addRel (NAT,(n1 + n2))
A1: (addRel (NAT,n1)) * (addRel (NAT,n2)) c= addRel (NAT,(n1 + n2)) by Th17;

now :: thesis: for x, y being object st [x,y] in addRel (NAT,(n1 + n2)) holds
[x,y] in (addRel (NAT,n1)) * (addRel (NAT,n2))

let x, y be object ; :: thesis: ( [x,y] in addRel (NAT,(n1 + n2)) implies [x,y] in (addRel (NAT,n1)) * (addRel (NAT,n2)) )
reconsider a = x, b = y as set by TARSKI:1;
assume A2: [x,y] in addRel (NAT,(n1 + n2)) ; :: thesis: [x,y] in (addRel (NAT,n1)) * (addRel (NAT,n2))
then [a,b] in addRel (NAT,(n1 + n2)) ;
then A3: ( a in NAT & b in NAT ) by MMLQUER2:4;
then reconsider a = a, b = b as Nat ;
A4: b = (n1 + n2) + a by A2, Th11;
set c = n1 + a;
( n1 + a in NAT & b = n2 + (n1 + a) ) by A4, ORDINAL1:def 12;
then ( [a,(n1 + a)] in addRel (NAT,n1) & [(n1 + a),b] in addRel (NAT,n2) ) by A3, Th11;
hence [x,y] in (addRel (NAT,n1)) * (addRel (NAT,n2)) by RELAT_1:def 8; :: thesis: verum

end;

then addRel (NAT,(n1 + n2)) c= (addRel (NAT,n1)) * (addRel (NAT,n2)) by RELAT_1:def 3;
hence (addRel (NAT,n1)) * (addRel (NAT,n2)) = addRel (NAT,(n1 + n2)) by A1, XBOOLE_0:def 10; :: thesis: verum