let A be transitive RelStr ; :: thesis: for B being finite Subset of A st not B is empty & the InternalRel of A is_connected_in B holds
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 ) )

let B be finite Subset of A; :: thesis: ( not B is empty & the InternalRel of A is_connected_in B implies 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 ) ) )

assume A1: ( not B is empty & the InternalRel of A is_connected_in B ) ; :: thesis: 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 ) )

defpred S1[ 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: S1[ {} ] ;
A4: for z, C being set st z in B & C c= B & S1[C] holds
S1[C \/ {z}]
proof
let z, C be set ; :: thesis: ( z in B & C c= B & S1[C] implies S1[C \/ {z}] )
assume that
A5: z in B and
A6: C c= B and
A7: S1[C] ; :: thesis: S1[C \/ {z}]
set D = C \/ {z};
per cases ( z in C or not z in C ) ;
suppose z in C ; :: thesis: S1[C \/ {z}]
then C \/ {z} = C by ;
hence S1[C \/ {z}] by A7; :: thesis: verum
end;
suppose A8: not z in C ; :: thesis: S1[C \/ {z}]
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 ( C is empty or not C is empty ) ;
suppose A11: C is empty ; :: 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 ) )

reconsider z = z as Element of A by A5;
take z ; :: thesis: ( z in C \/ {z} & ( for y being Element of A st y in C \/ {z} & z <> y holds
y <= z ) )

thus z in C \/ {z} by A9; :: thesis: for y being Element of A st y in C \/ {z} & z <> y holds
y <= z

let y be Element of A; :: thesis: ( y in C \/ {z} & z <> y implies y <= z )
assume ( y in C \/ {z} & z <> y ) ; :: thesis: y <= z
hence y <= z by ; :: thesis: verum
end;
suppose A12: not C is empty ; :: 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 ) )

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 then ( x <= z or z <= x ) by A1, A13, A5, A14, Th26;
suppose A15: x <= z ; :: 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 ) )

take z ; :: thesis: ( z in C \/ {z} & ( for y being Element of A st y in C \/ {z} & z <> y holds
y <= z ) )

thus z in C \/ {z} by A9; :: thesis: for y being Element of A st y in C \/ {z} & z <> y holds
y <= z

let y be Element of A; :: thesis: ( y in C \/ {z} & z <> y implies y <= z )
assume that
A16: y in C \/ {z} and
A17: z <> y ; :: thesis: y <= z
per cases ( y = x or y <> x ) ;
suppose y = x ; :: thesis: y <= z
hence y <= z by A15; :: thesis: verum
end;
suppose A18: y <> x ; :: thesis: y <= z
y in C by ;
then y <= x by ;
hence y <= z by ; :: thesis: verum
end;
end;
end;
suppose A19: z <= x ; :: 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 ) )

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

thus x in C \/ {z} by ; :: thesis: for y being Element of A st y in C \/ {z} & x <> y holds
y <= x

let y be Element of A; :: thesis: ( y in C \/ {z} & x <> y implies y <= x )
assume that
A20: y in C \/ {z} and
A21: x <> y ; :: thesis: y <= x
per cases ( y = z or y <> z ) ;
suppose y = z ; :: thesis: y <= x
hence y <= x by A19; :: thesis: verum
end;
suppose y <> z ; :: thesis: y <= x
then y in C by ;
hence y <= x by ; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
hence S1[C \/ {z}] ; :: thesis: verum
end;
end;
end;
S1[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: verum