theorem Th35: :: WAYBEL_4:35

for L being Semilattice
for I being Ideal of L holds DownMap I in the carrier of (MonSet L)