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 [(x \ u),(y \ u)] in P
let x, y be Element of X; :: thesis: ( [x,y] in P implies for u being Element of X holds [(x \ u),(y \ u)] in P )
assume A1: [x,y] in P ; :: thesis: for u being Element of X holds [(x \ u),(y \ u)] in P
let u be Element of X; :: thesis: [(x \ u),(y \ u)] in P
( x \ u = y \ u & x \ u in the carrier of X ) by A1, RELAT_1:def 10;
hence [(x \ u),(y \ u)] in P by RELAT_1:def 10; :: thesis: verum