theorem Th5: :: RCOMP_3:5

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