theorem :: WAYBEL24:2

for S being non empty RelStr
for T being non empty reflexive antisymmetric lower-bounded RelStr holds Bottom (MonMaps (S,T)) = S --> (Bottom T)