theorem Th24: :: PARTIT1:24

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