theorem Th7: :: HILB10_7:7

for X, Y1, Y2 being set holds UNION (X,(Y1 \/ Y2)) = (UNION (X,Y1)) \/ (UNION (X,Y2))