for L being non empty RelStr
for X being set holds
( ( ex_sup_of X,L implies ex_sup_of X /\ the carrier of L,L ) & ( ex_sup_of X /\ the carrier of L,L implies ex_sup_of X,L ) & ( ex_inf_of X,L implies ex_inf_of X /\ the carrier of L,L ) & ( ex_inf_of X /\ the carrier of L,L implies ex_inf_of X,L ) )