let n1, n2 be Element of NAT ; :: thesis: ( ( for e1, e2 being Equivalence_Relation of X
for x, y being object st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of X st
( len F = n1 + 2 & x,y are_joint_by F,e1,e2 ) ) & ex e1, e2 being Equivalence_Relation of X ex x, y being object st
( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & ( for F being non empty FinSequence of X holds
( not len F = n1 + 1 or not x,y are_joint_by F,e1,e2 ) ) ) & ( for e1, e2 being Equivalence_Relation of X
for x, y being object st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of X st
( len F = n2 + 2 & x,y are_joint_by F,e1,e2 ) ) & ex e1, e2 being Equivalence_Relation of X ex x, y being object st
( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & ( for F being non empty FinSequence of X holds
( not len F = n2 + 1 or not x,y are_joint_by F,e1,e2 ) ) ) implies n1 = n2 )
assume A24: for e1, e2 being Equivalence_Relation of X
for x, y being object st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of X st
( len F = n1 + 2 & x,y are_joint_by F,e1,e2 ) ; :: thesis: ( for e1, e2 being Equivalence_Relation of X
for x, y being object holds
( not e1 in the carrier of Y or not e2 in the carrier of Y or not [x,y] in e1 "\/" e2 or ex F being non empty FinSequence of X st
( len F = n1 + 1 & x,y are_joint_by F,e1,e2 ) ) or ex e1, e2 being Equivalence_Relation of X ex x, y being object st
( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & ( for F being non empty FinSequence of X holds
( not len F = n2 + 2 or not x,y are_joint_by F,e1,e2 ) ) ) or for e1, e2 being Equivalence_Relation of X
for x, y being object holds
( not e1 in the carrier of Y or not e2 in the carrier of Y or not [x,y] in e1 "\/" e2 or ex F being non empty FinSequence of X st
( len F = n2 + 1 & x,y are_joint_by F,e1,e2 ) ) or n1 = n2 )
given e19, e29 being Equivalence_Relation of X, x9, y9 being object such that A25: ( e19 in the carrier of Y & e29 in the carrier of Y & [x9,y9] in e19 "\/" e29 ) and
A26: for F being non empty FinSequence of X holds
( not len F = n1 + 1 or not x9,y9 are_joint_by F,e19,e29 ) ; :: thesis: ( ex e1, e2 being Equivalence_Relation of X ex x, y being object st
( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & ( for F being non empty FinSequence of X holds
( not len F = n2 + 2 or not x,y are_joint_by F,e1,e2 ) ) ) or for e1, e2 being Equivalence_Relation of X
for x, y being object holds
( not e1 in the carrier of Y or not e2 in the carrier of Y or not [x,y] in e1 "\/" e2 or ex F being non empty FinSequence of X st
( len F = n2 + 1 & x,y are_joint_by F,e1,e2 ) ) or n1 = n2 )
assume for e1, e2 being Equivalence_Relation of X
for x, y being object st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of X st
( len F = n2 + 2 & x,y are_joint_by F,e1,e2 ) ; :: thesis: ( for e1, e2 being Equivalence_Relation of X
for x, y being object holds
( not e1 in the carrier of Y or not e2 in the carrier of Y or not [x,y] in e1 "\/" e2 or ex F being non empty FinSequence of X st
( len F = n2 + 1 & x,y are_joint_by F,e1,e2 ) ) or n1 = n2 )
then A27: ex F2 being non empty FinSequence of X st
( len F2 = n2 + 2 & x9,y9 are_joint_by F2,e19,e29 ) by A25;
field e29 = X by EQREL_1:9;
then A28: e29 is_reflexive_in X by RELAT_2:def 9;
field e19 = X by EQREL_1:9;
then A29: e19 is_reflexive_in X by RELAT_2:def 9;
given e1, e2 being Equivalence_Relation of X, x, y being object such that A30: ( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 ) and
A31: for F being non empty FinSequence of X holds
( not len F = n2 + 1 or not x,y are_joint_by F,e1,e2 ) ; :: thesis: n1 = n2
A32: ex F1 being non empty FinSequence of X st
( len F1 = n1 + 2 & x,y are_joint_by F1,e1,e2 ) by A24, A30;
field e2 = X by EQREL_1:9;
then A33: e2 is_reflexive_in X by RELAT_2:def 9;
field e1 = X by EQREL_1:9;
then A34: e1 is_reflexive_in X by RELAT_2:def 9;
assume A35: not n1 = n2 ; :: thesis: contradiction

per cases ( n1 < n2 or n2 < n1 ) by A35, XXREAL_0:1;

suppose n1 < n2 ; :: thesis: contradiction

then n1 + 2 < n2 + (1 + 1) by XREAL_1:6;
then n1 + 2 < (n2 + 1) + 1 ;
then n1 + 2 <= n2 + 1 by NAT_1:13;
hence contradiction by A31, A32, A34, A33, Th12; :: thesis: verum

end;

suppose n2 < n1 ; :: thesis: contradiction

then n2 + 2 < n1 + (1 + 1) by XREAL_1:6;
then n2 + 2 < (n1 + 1) + 1 ;
then n2 + 2 <= n1 + 1 by NAT_1:13;
hence contradiction by A26, A27, A29, A28, Th12; :: thesis: verum

end;

end;