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