let IT1, IT2 be Relation of Class (EqRel R); :: thesis: ( ( for A, B being set 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 set 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
A9:
for A, B being set 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
A10:
for A, B being set 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 let x be
set ;
:: 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 A11:
x in IT1
;
:: thesis: x in IT2set Y =
Class (EqRel R);
consider A,
B being
set such that
A in Class (EqRel R)
and
B in Class (EqRel R)
and A12:
x = [A,B]
by A11, ZFMISC_1:def 2;
consider a,
b being
Element of
R such that A13:
(
A = Class (EqRel R),
a &
B = Class (EqRel R),
b &
a <= b )
by A9, A11, A12;
thus
x in IT2
by A10, A12, A13;
:: thesis: verum
end; assume A14:
x in IT2
;
:: thesis: x in IT1set Y =
Class (EqRel R);
consider A,
B being
set such that
(
A in Class (EqRel R) &
B in Class (EqRel R) )
and A15:
x = [A,B]
by A14, ZFMISC_1:def 2;
consider a,
b being
Element of
R such that A16:
(
A = Class (EqRel R),
a &
B = Class (EqRel R),
b &
a <= b )
by A10, A14, A15;
thus
x in IT1
by A9, A15, A16;
:: thesis: verum end;
hence
IT1 = IT2
by TARSKI:2; :: thesis: verum