:: deftheorem defines Real>=0 GRAPH_5:def 12 :
Real>=0 = { r where r is Real : r >= 0 } ;