theorem Th5: :: PARTIT_2:5

for Y being non empty set
for P being a_partition of Y
for x, y being Element of Y holds
( [x,y] in ERl P iff x in EqClass (y,P) )