theorem Th14: :: UNIFORM3:30

for X being set
for D being a_partition of X holds { (union P) where P is Subset of D : verum } = UniCl D