reconsider P = id the carrier of X as Equivalence_Relation of X ;
take P ; :: thesis: 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; :: thesis: ( [x,y] in P implies for u being Element of X holds [(u \ x),(u \ y)] in P )
assume A1: [x,y] in P ; :: thesis: for u being Element of X holds [(u \ x),(u \ y)] in P
let u be Element of X; :: thesis: [(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; :: thesis: verum