for S being non empty RelStr
for T being non empty antisymmetric lower-bounded RelStr holds Bottom (T |^ the carrier of S) = S --> (Bottom T)