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