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
x <= y ) )

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
x <= y ) ) )

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
x <= y ) )

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
x <= y ) ) );
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
x <= y ) )
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
x <= y ) ) ) 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
x <= y ) )

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
z <= y ) )

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

let y be Element of A; :: thesis: ( y in C \/ {z} & z <> y implies z <= y )
assume ( y in C \/ {z} & z <> y ) ; :: thesis: z <= y
hence z <= y 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
x <= y ) )

A13: not A is empty by A5;
A14: x in B by A12, A10, A6;
reconsider z = z as Element of A by A5;
z <> x by A12, A8, A10;
per cases then ( z <= x or x <= z ) by A1, A13, A5, A14, Th26;
suppose A15: 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
x <= y ) )

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

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

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

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

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

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