theorem :: WAYBEL_4:27

for L being lower-bounded sup-Semilattice
for AR being auxiliary Relation of L holds [( the carrier of L --> {(Bottom L)}),(AR -below)] in the InternalRel of (MonSet L)