for L1 being lower-bounded continuous sup-Semilattice st L1 is infinite holds
for B1 being with_bottom CLbasis of L1 holds B1 is infinite