theorem Th1: :: WAYBEL30:1

for x being set
for D being non empty set holds x /\ (union D) = union { (x /\ d) where d is Element of D : verum }