:: deftheorem defines positive XXREAL_0:def 6 :
for a being ExtReal holds
( a is positive iff a > 0 );