theorem Th31: :: ORDERS_5:22

for A being transitive RelStr
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 ) )