let L1 be continuous sup-Semilattice; :: thesis: for B1 being with_bottom CLbasis of L1 holds CLweight L1 c= card B1
let B1 be with_bottom CLbasis of L1; :: thesis: CLweight L1 c= card B1
card B1 in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } ;
hence CLweight L1 c= card B1 by SETFAM_1:3; :: thesis: verum