let A be Subset of [:RNS_Real,RNS_Real:]; :: thesis: ( ( for a, b being Real st [a,b] in A holds
ex Rx being real-membered set st
( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) } ) ) implies ex F being Function of A,REAL st
for a, b being Real st [a,b] in A holds
ex Rx being real-membered set st
( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) } & F . [a,b] = (upper_bound Rx) / 2 ) )
assume A1: for a, b being Real st [a,b] in A holds
ex Rx being real-membered set st
( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) } ) ; :: thesis: ex F being Function of A,REAL st
for a, b being Real st [a,b] in A holds
ex Rx being real-membered set st
( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) } & F . [a,b] = (upper_bound Rx) / 2 )
defpred S₁[ object , object ] means ex a, b being Real ex Rx being real-membered set st
( $1 = [a,b] & not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) } & $2 = (upper_bound Rx) / 2 );
A2: for x being object st x in A holds
ex y being object st
( y in REAL & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in A implies ex y being object st
( y in REAL & S₁[x,y] ) )
assume A3: x in A ; :: thesis: ex y being object st
( y in REAL & S₁[x,y] )
then consider a1, b1 being Point of RNS_Real such that
A4: x = [a1,b1] by PRVECT_3:18;
reconsider a = a1, b = b1 as Real ;
consider Rx being real-membered set such that
A5: ( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) } ) by A1, A3, A4;
take y = (upper_bound Rx) / 2; :: thesis: ( y in REAL & S₁[x,y] )
thus y in REAL by XREAL_0:def 1; :: thesis: S₁[x,y]
thus S₁[x,y] by A4, A5; :: thesis: verum

end;

consider F being Function of A,REAL such that
A6: for x being object st x in A holds
S₁[x,F . x] from FUNCT_2:sch 1(A2);
take F ; :: thesis: for a, b being Real st [a,b] in A holds
ex Rx being real-membered set st
( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) } & F . [a,b] = (upper_bound Rx) / 2 )
thus for a, b being Real st [a,b] in A holds
ex Rx being real-membered set st
( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) } & F . [a,b] = (upper_bound Rx) / 2 ) :: thesis: verum

proof

let a, b be Real; :: thesis: ( [a,b] in A implies ex Rx being real-membered set st
( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) } & F . [a,b] = (upper_bound Rx) / 2 ) )
assume [a,b] in A ; :: thesis: ex Rx being real-membered set st
( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) } & F . [a,b] = (upper_bound Rx) / 2 )
then consider a1, b1 being Real, Rx being real-membered set such that
A7: ( [a,b] = [a1,b1] & not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(a1 - r),(a1 + r).[,].(b1 - r),(b1 + r).[:] c= A ) } & F . [a,b] = (upper_bound Rx) / 2 ) by A6;
( a = a1 & b = b1 ) by A7, XTUPLE_0:1;
hence ex Rx being real-membered set st
( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) } & F . [a,b] = (upper_bound Rx) / 2 ) by A7; :: thesis: verum

end;