for L being lower-bounded sup-Semilattice
for AR being auxiliary Relation of L holds AR -below <= IdsMap L