theorem Th1: :: INTEGR26:1

for I being Interval st inf I in I holds
inf I = lower_bound I