1 in b by Lm1, Th25;
then A1: exp a,1 c= exp a,b by CARD_3:138;
( exp a,1 = a & omega c= a ) by Th25, CARD_2:40;
then omega c= exp a,b by A1, XBOOLE_1:1;
hence not exp a,b is finite ; :: thesis: verum