for L being non empty antisymmetric lower-bounded RelStr
for S being with_bottom Subset of L holds subrelstr S is lower-bounded