let a, b be Aleph; ( a c= b implies exp (a,b) = exp (2,b) )
A1:
card (bool a) = exp (2,(card a))
by CARD_2:31;
( card a = a & card a in card (bool a) )
by CARD_1:14;
then A2:
exp (a,b) c= exp ((exp (2,a)),b)
by A1, CARD_2:92;
assume
a c= b
; exp (a,b) = exp (2,b)
then A3:
( exp ((exp (2,a)),b) = exp (2,(a *` b)) & a *` b = b )
by Th17, CARD_2:30;
2 in a
by Lm2, Th15;
then
exp (2,b) c= exp (a,b)
by CARD_2:92;
hence
exp (a,b) = exp (2,b)
by A2, A3; verum