let n1, n2 be Element of NAT ; :: thesis: ( ( for e1, e2 being Equivalence_Relation of X
for x, y being set 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 set 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 set 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 set 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 A29: for e1, e2 being Equivalence_Relation of X
for x, y being set 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 set 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 set 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 set 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 e1', e2' being Equivalence_Relation of X, x', y' being set 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 = n1 + 1 or not x',y' are_joint_by F,e1',e2' ) ; :: thesis: ( ex e1, e2 being Equivalence_Relation of X ex x, y being set 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 set 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 A32: for e1, e2 being Equivalence_Relation of X
for x, y being set 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 set 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 e1, e2 being Equivalence_Relation of X, x, y being set such that A33: ( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 ) and
A34: 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
consider F1 being non empty FinSequence of X such that
A35: ( len F1 = n1 + 2 & x,y are_joint_by F1,e1,e2 ) by A29, A33;
consider F2 being non empty FinSequence of X such that
A36: ( len F2 = n2 + 2 & x',y' are_joint_by F2,e1',e2' ) by A30, A32;
( field e1 = X & field e2 = X ) by EQREL_1:16;
then A37: ( e1 is_reflexive_in X & e2 is_reflexive_in X ) by RELAT_2:def 9;
( field e1' = X & field e2' = X ) by EQREL_1:16;
then A38: ( e1' is_reflexive_in X & e2' is_reflexive_in X ) by RELAT_2:def 9;
assume A39: not n1 = n2 ; :: thesis: contradiction

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

suppose n1 < n2 ; :: thesis: contradiction

then n1 + 2 < n2 + (1 + 1) by XREAL_1:8;
then n1 + 2 < (n2 + 1) + 1 ;
then n1 + 2 <= n2 + 1 by NAT_1:13;
hence contradiction by A34, A35, A37, Th14; :: thesis: verum

end;

suppose n2 < n1 ; :: thesis: contradiction

then n2 + 2 < n1 + (1 + 1) by XREAL_1:8;
then n2 + 2 < (n1 + 1) + 1 ;
then n2 + 2 <= n1 + 1 by NAT_1:13;
hence contradiction by A31, A36, A38, Th14; :: thesis: verum

end;

end;