theorem :: YELLOW_0:44

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