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