theorem :: WAYBEL_4:5

for L being lower-bounded sup-Semilattice holds Bottom (InclPoset (Aux L)) = AuxBottom L