theorem :: FUZZY_6:7

for a, b, c being Real st a < b holds
( ['a,b'] c= [#] REAL & lower_bound ['a,b'] = a & upper_bound ['a,b'] = b )