:: deftheorem Def3 defines [' INTEGRA5:def 3 :
for a, b being Real st a <= b holds
['a,b'] = [.a,b.];