theorem :: YELLOW_4:22

for L being reflexive antisymmetric with_suprema RelStr
for D being Subset of L
for x being Element of L st x is_<=_than D holds
{x} "\/" D = D