theorem :: WAYBEL_6:21

for L being non empty antisymmetric lower-bounded RelStr holds Bottom L is co-prime