let a, b be set ; :: thesis: ( <*a,b*> in y>=0-plane iff ( a in REAL & ex y being Real st
( b = y & y >= 0 ) ) )

hereby :: thesis: ( a in REAL & ex y being Real st
( b = y & y >= 0 ) implies <*a,b*> in y>=0-plane )

assume <*a,b*> in y>=0-plane ; :: thesis: ( 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 XREAL_0:def 1; :: thesis: ex y being Real st
( b = y & y >= 0 )
take y = y; :: thesis: ( b = y & y >= 0 )
<*a,b*> . 2 = b ;
hence ( b = y & y >= 0 ) by A3, A2, FINSEQ_1:44; :: thesis: verum

end;

assume a in REAL ; :: thesis: ( 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 ; :: thesis: <*a,b*> in y>=0-plane
|[x,y]| = <*a,b*> by A4;
hence <*a,b*> in y>=0-plane by A5; :: thesis: verum