theorem Th4: :: WAYBEL11:4

for T being with_suprema Poset
for D being non empty finite directed Subset of T holds sup D in D