theorem Th45: :: INTERVA1:45

for U being non empty set
for A being non empty IntervalSet of U holds A ^ = Inter (((A ``2) `),((A ``1) `)) by Th41;