:: deftheorem defines negative XXREAL_0:def 7 :
for a being ExtReal holds
( a is negative iff a < 0 );