theorem Th1: :: WAYBEL_0:1

for L being non empty transitive RelStr
for X being Subset of L holds
( ( not X is empty & X is directed ) iff for Y being finite Subset of X ex x being Element of L st
( x in X & x is_>=_than Y ) )