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) )

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

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 )

y in EqClass (y,P)
by EQREL_1:def 6;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;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

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