theorem Th7: :: RCOMP_3:7

for r, s being Real st r < s holds
upper_bound ].r,s.] = s