for L being non empty antisymmetric lower-bounded RelStr
for x being Element of L holds Bottom L <= x