let n be Nat; :: thesis: addRel (NAT,n) = { [n1,(n1 + n)] where n1 is Nat : verum }
set S = { [n1,(n1 + n)] where n1 is Nat : verum } ;

now :: thesis: for o being object holds
( ( o in addRel (NAT,n) implies o in { [n1,(n1 + n)] where n1 is Nat : verum } ) & ( o in { [n1,(n1 + n)] where n1 is Nat : verum } implies o in addRel (NAT,n) ) )

let o be object ; :: thesis: ( ( o in addRel (NAT,n) implies o in { [n1,(n1 + n)] where n1 is Nat : verum } ) & ( o in { [n1,(n1 + n)] where n1 is Nat : verum } implies o in addRel (NAT,n) ) )

hereby :: thesis: ( o in { [n1,(n1 + n)] where n1 is Nat : verum } implies o in addRel (NAT,n) )

assume A1: o in addRel (NAT,n) ; :: thesis: o in { [n1,(n1 + n)] where n1 is Nat : verum }
then consider x, y being object such that
A2: o = [x,y] by RELAT_1:def 1;
reconsider x = x, y = y as set by TARSKI:1;
[x,y] in addRel (NAT,n) by A1, A2;
then ( x in NAT & y in NAT ) by MMLQUER2:4;
then reconsider x = x, y = y as Nat ;
y = n + x by A1, A2, Th11;
hence o in { [n1,(n1 + n)] where n1 is Nat : verum } by A2; :: thesis: verum

end;

assume o in { [n1,(n1 + n)] where n1 is Nat : verum } ; :: thesis: o in addRel (NAT,n)
then consider n1 being Nat such that
A3: o = [n1,(n1 + n)] ;
( n1 in NAT & n1 + n in NAT ) by ORDINAL1:def 12;
hence o in addRel (NAT,n) by A3, Th11; :: thesis: verum

end;

hence addRel (NAT,n) = { [n1,(n1 + n)] where n1 is Nat : verum } by TARSKI:2; :: thesis: verum