let IT1, IT2 be Relation of (Class (EqRel R)); :: thesis: ( ( 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 ) ) ; :: thesis: IT1 = IT2

now :: thesis: for x being object holds
( ( x in IT1 implies x in IT2 ) & ( x in IT2 implies x in IT1 ) )

let x be object ; :: thesis: ( ( x in IT1 implies x in IT2 ) & ( x in IT2 implies x in IT1 ) )

hereby :: thesis: ( x in IT2 implies x in IT1 )

assume A12: x in IT1 ; :: thesis: x in IT2
set Y = Class (EqRel R);
consider A, B being object such that
A in Class (EqRel R) and
B in Class (EqRel R) and
A13: x = [A,B] by A12, ZFMISC_1:def 2;
ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) by A10, A12, A13;
hence x in IT2 by A11, A13; :: thesis: verum

end;

assume A14: x in IT2 ; :: thesis: x in IT1
set Y = Class (EqRel R);
consider A, B being object such that
A in Class (EqRel R) and
B in Class (EqRel R) and
A15: x = [A,B] by A14, ZFMISC_1:def 2;
ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) by A11, A14, A15;
hence x in IT1 by A10, A15; :: thesis: verum

end;

hence IT1 = IT2 by TARSKI:2; :: thesis: verum