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

the InternalRel of A is_connected_in B by Def1, Th16;

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, Th33; :: thesis: verum

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 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 ; :: 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 ) )

the InternalRel of A is_connected_in B by Def1, Th16;

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, Th33; :: thesis: verum