let r be Real; :: thesis: multRel (REAL,r) = { [r1,(r1 * r)] where r1 is Real : verum }
set S = { [r1,(r1 * r)] where r1 is Real : verum } ;

now :: thesis: for o being object holds
( ( o in multRel (REAL,r) implies o in { [r1,(r1 * r)] where r1 is Real : verum } ) & ( o in { [r1,(r1 * r)] where r1 is Real : verum } implies o in multRel (REAL,r) ) )

let o be object ; :: thesis: ( ( o in multRel (REAL,r) implies o in { [r1,(r1 * r)] where r1 is Real : verum } ) & ( o in { [r1,(r1 * r)] where r1 is Real : verum } implies o in multRel (REAL,r) ) )

hereby :: thesis: ( o in { [r1,(r1 * r)] where r1 is Real : verum } implies o in multRel (REAL,r) )

assume A1: o in multRel (REAL,r) ; :: thesis: o in { [r1,(r1 * r)] where r1 is Real : 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 multRel (REAL,r) by A1, A2;
then ( x in REAL & y in REAL ) by MMLQUER2:4;
then reconsider x = x, y = y as Real ;
y = r * x by A1, A2, Th42;
hence o in { [r1,(r1 * r)] where r1 is Real : verum } by A2; :: thesis: verum

end;

assume o in { [r1,(r1 * r)] where r1 is Real : verum } ; :: thesis: o in multRel (REAL,r)
then consider r1 being Real such that
A3: o = [r1,(r1 * r)] ;
( r1 in REAL & r1 * r in REAL ) by XREAL_0:def 1;
hence o in multRel (REAL,r) by A3, Th42; :: thesis: verum

end;

hence multRel (REAL,r) = { [r1,(r1 * r)] where r1 is Real : verum } by TARSKI:2; :: thesis: verum