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