theorem :: BVFUNC11:2

for Y being non empty set
for z being Element of Y
for PA, PB being a_partition of Y holds EqClass (z,PA) c= EqClass (z,(PA '\/' PB)) by Th1, PARTIT1:16;