let L1 be lower-bounded continuous sup-Semilattice; :: thesis: ( L1 is infinite implies for B1 being with_bottom CLbasis of L1 holds B1 is infinite )
assume A1: L1 is infinite ; :: thesis: for B1 being with_bottom CLbasis of L1 holds B1 is infinite
let B1 be with_bottom CLbasis of L1; :: thesis: B1 is infinite
( dom (supMap (subrelstr B1)) = Ids (subrelstr B1) & rng (supMap (subrelstr B1)) = the carrier of L1 ) by WAYBEL23:51, WAYBEL23:65;
then card the carrier of L1 c= card (Ids (subrelstr B1)) by CARD_1:12;
then Ids (subrelstr B1) is infinite by A1;
then subrelstr B1 is infinite by Th16;
hence B1 is infinite by YELLOW_0:def 15; :: thesis: verum