theorem Th29: :: YELLOW_4:29

for L being antisymmetric with_suprema RelStr
for X being Subset of L
for Y being non empty Subset of L holds X c= downarrow (X "\/" Y)