for L being non empty antisymmetric upper-bounded RelStr holds
( ex_inf_of {} ,L & ex_sup_of the carrier of L,L )