theorem Th6: :: MESFUN17:6

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