let a, b, c be Ordinal; ( 0 in a & 1 in b & a in exp (b,c) implies b -exponent a in c )
assume that
A1:
0 in a
and
A2:
1 in b
and
A3:
a in exp (b,c)
; b -exponent a in c
( exp (b,c) = 1 *^ (exp (b,c)) & 0 in 1 )
by CARD_1:49, TARSKI:def 1, ORDINAL2:39;
then
b -exponent (exp (b,c)) = c
by A2, ORDINAL5:58;
then A4:
b -exponent a c= c
by A3, Th22, ORDINAL1:def 2;
b -exponent a <> c
hence
b -exponent a in c
by A4, XBOOLE_0:def 8, ORDINAL1:11; verum