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 8; :: thesis: verum

end;

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