:: deftheorem defines y>=0-plane TOPGEN_5:def 2 :
y>=0-plane = { |[x,y]| where x, y is Real : y >= 0 } ;