theorem :: WAYBEL_4:16

for L being lower-bounded sup-Semilattice holds MonSet L is full SubRelStr of (InclPoset (Ids L)) |^ the carrier of L