for Y being non empty set
for P, Q, R being a_partition of Y st ERl R = (ERl P) * (ERl Q) holds
for x, y being Element of Y holds
( x in EqClass (y,R) iff ex z being Element of Y st
( x in EqClass (z,P) & z in EqClass (y,Q) ) )