theorem :: WAYBEL12:13

for L being antisymmetric upper-bounded with_suprema RelStr
for X being non empty Subset of L holds X "\/" {(Top L)} = {(Top L)}