theorem Th25: :: WAYBEL_4:25

for L being lower-bounded sup-Semilattice holds the carrier of L --> {(Bottom L)} is Function of L,(InclPoset (Ids L))