theorem Th46: :: INTERVA1:46

for U being non empty set
for A being non empty IntervalSet of U
for X, Y being Subset of U st A = Inter (X,Y) & X c= Y holds
A ^ = Inter ((Y `),(X `))