for L being non empty reflexive antisymmetric RelStr
for a being Element of L holds
( ex_sup_of {a},L & ex_inf_of {a},L )