theorem Th16: :: YELLOW_2:16

for L being with_suprema Poset
for f being Function of L,L st f is directed-sups-preserving holds
f is monotone