let a, b be Real; :: thesis: ( |[a,b]| in y>=0-plane iff b >= 0 )
( |[a,b]| in y>=0-plane iff ex x, y being Real st
( |[a,b]| = |[x,y]| & y >= 0 ) ) ;
hence ( |[a,b]| in y>=0-plane iff b >= 0 ) by SPPOL_2:1; :: thesis: verum