:: deftheorem Def2 defines (#) TREAL_1:def 2 :
for a, b being Real st a <= b holds
(a,b) (#) = b;