for L being non empty antisymmetric complete RelStr
for X being set holds
( ex_sup_of X,L & ex_inf_of X,L )