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