for L being non empty reflexive antisymmetric RelStr holds
( L is up-complete iff for X being non empty directed Subset of L holds ex_sup_of X,L )