theorem Th4: :: RCOMP_3:4

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