let a, b be real number ; :: thesis: ( |[a,b]| in y>=0-plane iff b >= 0 )
( ( |[a,b]| in y>=0-plane implies ex x, y being Element of REAL st
( |[a,b]| = |[x,y]| & y >= 0 ) ) & ( ex x, y being Element of REAL st
( |[a,b]| = |[x,y]| & y >= 0 ) implies |[a,b]| in y>=0-plane ) & a is Real & b is Real ) by XREAL_0:def 1;
hence ( |[a,b]| in y>=0-plane iff b >= 0 ) by SPPOL_2:1; :: thesis: verum