let A be Subset of [:RNS_Real,RNS_Real,RNS_Real:]; :: thesis: ( ( for a, b, c being Real st [a,b,c] 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 - r),(c + r).[:] c= A ) } ) ) implies ex F being Function of A,REAL st
for a, b, c being Real st [a,b,c] 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 - r),(c + r).[:] c= A ) } & F . [a,b,c] = (upper_bound Rx) / 2 ) )
assume A1: for a, b, c being Real st [a,b,c] 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 - r),(c + r).[:] c= A ) } ) ; :: thesis: ex F being Function of A,REAL st
for a, b, c being Real st [a,b,c] 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 - r),(c + r).[:] c= A ) } & F . [a,b,c] = (upper_bound Rx) / 2 )
defpred S₁[ object , object ] means ex a, b, c being Real ex Rx being real-membered set st
( $1 = [a,b,c] & 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 - r),(c + 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, c1 being Point of RNS_Real such that
A4: x = [a1,b1,c1] by PRVECT_4:9;
reconsider a = a1, b = b1, c = c1 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 - r),(c + 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, c being Real st [a,b,c] 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 - r),(c + r).[:] c= A ) } & F . [a,b,c] = (upper_bound Rx) / 2 )
thus for a, b, c being Real st [a,b,c] 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 - r),(c + r).[:] c= A ) } & F . [a,b,c] = (upper_bound Rx) / 2 ) :: thesis: verum

proof

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

end;