theorem Th34: :: INTERVA1:34

for X being set
for A, B being non empty ordered Subset-Family of X holds UNION ((INTERSECTION (A,B)),B) = B