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