for L1 being lower-bounded continuous sup-Semilattice st L1 is infinite holds
for B1 being with_bottom CLbasis of L1 holds card { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } c= card B1