let IT1, IT2 be Relation of (Class (EqRel R)); ( ( for A, B being object holds
( [A,B] in IT1 iff ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) ) ) & ( for A, B being object holds
( [A,B] in IT2 iff ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) ) ) implies IT1 = IT2 )
assume that
A10:
for A, B being object holds
( [A,B] in IT1 iff ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) )
and
A11:
for A, B being object holds
( [A,B] in IT2 iff ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) )
; IT1 = IT2
now for x being object holds
( ( x in IT1 implies x in IT2 ) & ( x in IT2 implies x in IT1 ) )end;
hence
IT1 = IT2
by TARSKI:2; verum