theorem Th33: :: ORDERS_5:24

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