let a, b be set ; ( <*a,b*> in y=0-line iff ( a in REAL & b = 0 ) )
A1:
( <*a,b*> in y=0-line iff ex x being Real st <*a,b*> = |[x,0]| )
;
hereby ( a in REAL & b = 0 implies <*a,b*> in y=0-line )
A2:
<*a,b*> . 1
= a
by FINSEQ_1:44;
assume
<*a,b*> in y=0-line
;
( a in REAL & b = 0 )then consider x,
y being
Real such that A3:
<*a,b*> = |[x,0]|
by A1;
<*a,b*> . 1
= x
by A3, FINSEQ_1:44;
hence
a in REAL
by A2, XREAL_0:def 1;
b = 0
<*a,b*> . 2
= b
by FINSEQ_1:44;
hence
b = 0
by A3, FINSEQ_1:44;
verum
end;
assume
a in REAL
; ( not b = 0 or <*a,b*> in y=0-line )
then reconsider x = a as Real ;
|[x,0]| = <*a,0*>
;
hence
( not b = 0 or <*a,b*> in y=0-line )
; verum