theorem Th6: :: RCOMP_3:6

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