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