theorem :: PARTIT1:26

for Y being non empty set
for PA, PB, PC being a_partition of Y holds (PA '\/' PB) '\/' PC = PA '\/' (PB '\/' PC)