theorem Th23: :: PARTIT1:23

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