theorem Th2: :: INTEGR26:2

for I being interval Subset of REAL st sup I in I holds
sup I = upper_bound I