let Y be non empty set ; :: thesis: 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) )
let P be a_partition of Y; :: thesis: for x, y being Element of Y holds
( [x,y] in ERl P iff x in EqClass (y,P) )
let x, y be Element of Y; :: thesis: ( [x,y] in ERl P iff x in EqClass (y,P) )

hereby :: thesis: ( x in EqClass (y,P) implies [x,y] in ERl P )

assume [x,y] in ERl P ; :: thesis: x in EqClass (y,P)
then ex A being Subset of Y st
( A in P & x in A & y in A ) by PARTIT1:def 6;
hence x in EqClass (y,P) by EQREL_1:def 6; :: thesis: verum

end;

y in EqClass (y,P) by EQREL_1:def 6;
hence ( x in EqClass (y,P) implies [x,y] in ERl P ) by PARTIT1:def 6; :: thesis: verum