defpred S₁[ Element of NAT ] means 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 = $1 + 2 & x,y are_joint_by F,e1,e2 );
set A = { n where n is Element of NAT : S₁[n] } ;
consider e1, e2 being Equivalence_Relation of X such that
A4: ( e1 = e & e2 = e ) ;
A5: field e = X by EQREL_1:9;
then id X c= e by RELAT_2:1;
then not e c= id X by A2;
then consider x, y being object such that
A6: [x,y] in e and
A7: not [x,y] in id X by RELAT_1:def 3;
A8: ( not x in X or x <> y ) by A7, RELAT_1:def 10;
A9: [x,y] in e1 "\/" e2 by A6, A4;
then consider F being non empty FinSequence of X such that
A10: len F = o and
A11: x,y are_joint_by F,e1,e2 by A1, A3, A4;
A12: ( F . 1 = x & F . (len F) = y ) by A11;
o >= 2

proof

assume not o >= 2 ; :: thesis: contradiction
then len F < 1 + 1 by A10;
then ( 0 <= len F & len F <= 0 + 1 ) by NAT_1:2, NAT_1:13;
hence contradiction by A5, A6, A8, A12, NAT_1:9, RELAT_1:15; :: thesis: verum

end;

then consider o9 being Nat such that
A13: o = 2 + o9 by NAT_1:10;
A14: { n where n is Element of NAT : S₁[n] } is Subset of NAT from DOMAIN_1:sch 7();
o9 in NAT by ORDINAL1:def 12;
then consider k being Element of NAT such that
k = o9 and
A15: 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 = k + 2 & x,y are_joint_by F,e1,e2 ) by A3, A13;
k in { n where n is Element of NAT : S₁[n] } by A15;
then reconsider A = { n where n is Element of NAT : S₁[n] } as non empty Subset of NAT by A14;
set m = min A;
A16: 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 = (min A) + 1 or not x,y are_joint_by F,e1,e2 ) ) )

proof

assume A17: 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 = (min A) + 1 & x,y are_joint_by F,e1,e2 ) ) ; :: thesis: contradiction
then consider F being non empty FinSequence of X such that
A18: len F = (min A) + 1 and
A19: x,y are_joint_by F,e1,e2 by A1, A4, A9;
A20: ( F . 1 = x & F . (len F) = y ) by A19;
len F >= 2

proof

assume not len F >= 2 ; :: thesis: contradiction
then len F < 1 + 1 ;
then ( 0 <= len F & len F <= 0 + 1 ) by NAT_1:2, NAT_1:13;
hence contradiction by A5, A6, A8, A20, NAT_1:9, RELAT_1:15; :: thesis: verum

end;

then (min A) + 1 >= 1 + 1 by A18;
then A21: min A >= 1 by XREAL_1:6;
then ( (min A) + 1 = ((min A) - 1) + 2 & (min A) - 1 = (min A) -' 1 ) by XREAL_1:233;
then A22: (min A) -' 1 in A by A17;
min A < (min A) + 1 by XREAL_1:29;
then A23: (min A) - 1 < ((min A) + 1) - 1 by XREAL_1:9;
(min A) - 1 >= 0 by A21, XREAL_1:48;
then (min A) -' 1 < min A by A23, XREAL_0:def 2;
hence contradiction by A22, XXREAL_2:def 7; :: thesis: verum

end;

min A in A by XXREAL_2:def 7;
then ex m9 being Element of NAT st
( m9 = min A & ( 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 = m9 + 2 & x,y are_joint_by F,e1,e2 ) ) ) ;
hence ex b₁ being Element of NAT st
( ( 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 = b₁ + 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 = b₁ + 1 or not x,y are_joint_by F,e1,e2 ) ) ) ) by A16; :: thesis: verum