theorem :: YELLOW_4:13

for L being reflexive antisymmetric with_suprema RelStr
for A being Subset of L holds A c= A "\/" A