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