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