theorem Th14: :: MESFUN16:14

for A being Subset of [:RNS_Real,RNS_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 ) } ) ) holds
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 )