theorem Th25: :: BORSUK_4:28

for C being non empty closed_interval Subset of REAL holds lower_bound C <= upper_bound C