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