let q be Rational; :: thesis: addRel (RAT,q) = { [q1,(q1 + q)] where q1 is Rational : verum }
set S = { [q1,(q1 + q)] where q1 is Rational : verum } ;

now :: thesis: for o being object holds
( ( o in addRel (RAT,q) implies o in { [q1,(q1 + q)] where q1 is Rational : verum } ) & ( o in { [q1,(q1 + q)] where q1 is Rational : verum } implies o in addRel (RAT,q) ) )

let o be object ; :: thesis: ( ( o in addRel (RAT,q) implies o in { [q1,(q1 + q)] where q1 is Rational : verum } ) & ( o in { [q1,(q1 + q)] where q1 is Rational : verum } implies o in addRel (RAT,q) ) )

hereby :: thesis: ( o in { [q1,(q1 + q)] where q1 is Rational : verum } implies o in addRel (RAT,q) )

assume A1: o in addRel (RAT,q) ; :: thesis: o in { [q1,(q1 + q)] where q1 is Rational : 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 (RAT,q) by A1, A2;
then ( x in RAT & y in RAT ) by MMLQUER2:4;
then reconsider x = x, y = y as Rational ;
y = q + x by A1, A2, Th11;
hence o in { [q1,(q1 + q)] where q1 is Rational : verum } by A2; :: thesis: verum

end;

assume o in { [q1,(q1 + q)] where q1 is Rational : verum } ; :: thesis: o in addRel (RAT,q)
then consider q1 being Rational such that
A3: o = [q1,(q1 + q)] ;
( q1 in RAT & q1 + q in RAT ) by RAT_1:def 2;
hence o in addRel (RAT,q) by A3, Th11; :: thesis: verum

end;

hence addRel (RAT,q) = { [q1,(q1 + q)] where q1 is Rational : verum } by TARSKI:2; :: thesis: verum