1 in b by Lm1, Th15;
then A1: exp (a,1) c= exp (a,b) by CARD_2:92;
( exp (a,1) = a & omega c= a ) by Th15, CARD_2:27;
then omega c= exp (a,b) by A1;
hence not exp (a,b) is finite ; :: thesis: verum