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

hereby :: thesis: ( a in REAL & ex y being Element of 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 Element of REAL st
( b = y & y >= 0 ) )
then consider x, y being Element of REAL such that
A1: ( <*a,b*> = |[x,y]| & y >= 0 ) ;
A2: ( <*a,b*> . 1 = a & <*a,b*> . 1 = x & <*a,b*> . 2 = b & <*a,b*> . 2 = y ) by A1, FINSEQ_1:61;
hence a in REAL ; :: thesis: ex y being Element of REAL st
( b = y & y >= 0 )
take y = y; :: thesis: ( b = y & y >= 0 )
thus ( b = y & y >= 0 ) by A1, A2; :: thesis: verum

end;

assume a in REAL ; :: thesis: ( for y being Element of 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 Element of REAL such that A3: ( b = y & y >= 0 ) ; :: thesis: <*a,b*> in y>=0-plane
|[x,y]| = <*a,b*> by A3;
hence <*a,b*> in y>=0-plane by A3; :: thesis: verum