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