theorem :: TOPGEN_5:17

for a, b being set holds
( <*a,b*> in y>=0-plane iff ( a in REAL & ex y being Real st
( b = y & y >= 0 ) ) )