theorem :: BVFUNC11:4

for Y being non empty set
for z being Element of Y
for PA being a_partition of Y holds
( EqClass (z,PA) c= EqClass (z,(%O Y)) & EqClass (z,(%I Y)) c= EqClass (z,PA) ) by Th1, PARTIT1:32;