theorem Th38: :: WAYBEL_0:38

for L being non empty reflexive transitive RelStr
for X being Subset of L st ex_inf_of X,L holds
inf X = inf (uparrow X)