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