let R be Equivalence_Relation of M; :: thesis: R is compatible
consider x being object such that
A1: the carrier of M = {x} by ZFMISC_1:131;
reconsider x = x as Element of M by A1, TARSKI:def 1;

now :: thesis: for v, v9, w, w9 being Element of M st v in Class (R,v9) & w in Class (R,w9) holds
v * w in Class (R,(v9 * w9))

let v, v9, w, w9 be Element of M; :: thesis: ( v in Class (R,v9) & w in Class (R,w9) implies v * w in Class (R,(v9 * w9)) )
assume ( v in Class (R,v9) & w in Class (R,w9) ) ; :: thesis: v * w in Class (R,(v9 * w9))
A2: ( v * w = x & v9 * w9 = x ) by A1, TARSKI:def 1;
v9 * w9 in Class (R,(v9 * w9)) by EQREL_1:20;
hence v * w in Class (R,(v9 * w9)) by A2; :: thesis: verum

end;

hence R is compatible ; :: thesis: verum