reconsider P = id the carrier of X as Equivalence_Relation of X ;
take
P
; for x, y being Element of X st [x,y] in P holds
for u being Element of X holds [(u \ x),(u \ y)] in P
let x, y be Element of X; ( [x,y] in P implies for u being Element of X holds [(u \ x),(u \ y)] in P )
assume A1:
[x,y] in P
; for u being Element of X holds [(u \ x),(u \ y)] in P
let u be Element of X; [(u \ x),(u \ y)] in P
u \ x = u \ y
by A1, RELAT_1:def 10;
hence
[(u \ x),(u \ y)] in P
by RELAT_1:def 10; verum