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