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