theorem :: YELLOW_0:54

for L being non empty Poset holds
( L is with_suprema iff for X being non empty finite Subset of L holds ex_sup_of X,L )