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

x <= y ) )

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

x <= y ) ) )

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

x <= y ) )

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

x <= y ) ) by A1, Th31; :: 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

x <= y ) )

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

x <= y ) ) )

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

x <= y ) )

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

x <= y ) ) by A1, Th31; :: thesis: verum