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:44;
( card a = a & card a in card (bool a) )
by CARD_1:30, CARD_1:def 5;
then A2:
exp (a,b) c= exp ((exp (2,a)),b)
by A1, CARD_3:138;
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 Th27, CARD_2:43;
2 in a
by Lm2, Th25;
then
exp (2,b) c= exp (a,b)
by CARD_3:138;
hence
exp (a,b) = exp (2,b)
by A2, A3, XBOOLE_0:def 10; verum