let L1 be lower-bounded continuous sup-Semilattice; :: thesis: ( not L1 is finite implies for B1 being with_bottom CLbasis of L1 holds not B1 is finite )
assume A1: not L1 is finite ; :: thesis: for B1 being with_bottom CLbasis of L1 holds not B1 is finite
let B1 be with_bottom CLbasis of L1; :: thesis: not B1 is finite
( 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 not Ids (subrelstr B1) is finite by A1;
then not subrelstr B1 is finite by Th19;
hence not B1 is finite by YELLOW_0:def 15; :: thesis: verum