:: deftheorem defines y=0-line TOPGEN_5:def 1 :
y=0-line = { |[x,0]| where x is Real : verum } ;