for L being non empty antisymmetric upper-bounded RelStr
for X being non empty Subset of L holds Top L in uparrow X