for L being non empty antisymmetric upper-bounded RelStr
for a being Element of L st Top L <= a holds
a = Top L