theorem Th51: :: WAYBEL_0:51

for L being non empty transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ) holds
F is directed