:: deftheorem defines _le_ PRSUBSET:def 5 :
for a, b being ExtReal holds a _le_ b = IFGT (a,b,FALSE,TRUE);