theorem Th30: :: INTERVA1:30

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