let A be transitive RelStr ; :: thesis:
let B be finite Subset of A; :: thesis:
assume A1: ( not B is empty & the InternalRel of A is_connected_in B ) ; :: thesis:
defpred S₁[ set ] means ( not $1 is empty implies ex x being Element of A st
( x in $1 & ( for y being Element of A st y in $1 & x <> y holds
y <= x ) ) );
A2: B is finite ;
A3: S₁[ {} ] ;
A4: for z, C being set st z in B & C c= B & S₁[C] holds
S₁[C \/ {z}]

proof

let z, C be set ; :: thesis:
assume that
A5: z in B and
A6: C c= B and
A7: S₁[C] ; :: thesis:
set D = C \/ {z};

per cases ;

suppose z in C ; :: thesis:

then C \/ {z} = C by ZFMISC_1:31, XBOOLE_1:12;
hence S₁[C \/ {z}] by A7; :: thesis:

end;

suppose A8: not z in C ; :: thesis:

ex x being Element of A st
( x in C \/ {z} & ( for y being Element of A st y in C \/ {z} & x <> y holds
y <= x ) )

proof

z in {z} by TARSKI:def 1;
then A9: z in C \/ {z} by XBOOLE_0:def 3;
consider x being Element of A such that
A10: ( not C is empty implies ( x in C & ( for y being Element of A st y in C & x <> y holds
y <= x ) ) ) by A7;

per cases ;

suppose A11: C is empty ; :: thesis:

reconsider z = z as Element of A by A5;
take z ; :: thesis:
thus z in C \/ {z} by A9; :: thesis:
let y be Element of A; :: thesis:
assume ( y in C \/ {z} & z <> y ) ; :: thesis:
hence y <= z by A11, TARSKI:def 1; :: thesis:

end;

suppose A12: not C is empty ; :: thesis:

A13: not A is empty by A5;
reconsider z = z as Element of A by A5;
A14: x in B by A12, A10, A6;
z <> x by A12, A8, A10;

per cases by A1, A13, A5, A14, Th26;

suppose A15: x <= z ; :: thesis:

take z ; :: thesis:
thus z in C \/ {z} by A9; :: thesis:
let y be Element of A; :: thesis:
assume that
A16: y in C \/ {z} and
A17: z <> y ; :: thesis:

per cases ;

suppose y = x ; :: thesis:

hence y <= z by A15; :: thesis:

end;

suppose A18: y <> x ; :: thesis:

y in C by A16, A17, ZFMISC_1:136;
then y <= x by A18, A10;
hence y <= z by A15, ORDERS_2:3; :: thesis:

end;

end;

end;

suppose A19: z <= x ; :: thesis:

take x ; :: thesis:
thus x in C \/ {z} by A12, A10, XBOOLE_0:def 3; :: thesis:
let y be Element of A; :: thesis:
assume that
A20: y in C \/ {z} and
A21: x <> y ; :: thesis:

per cases ;

suppose y = z ; :: thesis:

hence y <= x by A19; :: thesis:

end;

suppose y <> z ; :: thesis:

then y in C by A20, ZFMISC_1:136;
hence y <= x by A21, A10; :: thesis:

end;

end;

end;

end;

end;

end;

end;

hence S₁[C \/ {z}] ; :: thesis:

end;

end;

end;

S₁[B] from FINSET_1:sch 2(A2, A3, A4);
hence ex x being Element of A st
( x in B & ( for y being Element of A st y in B & x <> y holds
y <= x ) ) by A1; :: thesis: