for L being non empty reflexive antisymmetric complete RelStr
for D being Subset of L
for x being Element of L st x in D holds
(sup D) "/\" x = x