for L being non empty RelStr st ( for A being Subset of L holds ex_sup_of A,L ) holds
for X being set holds
( ex_sup_of X,L & "\/" (X,L) = "\/" ((X /\ the carrier of L),L) )