let a, b, c be Ordinal; :: thesis: ( 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) ; :: thesis: 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

proof

assume A5: b -exponent a = c ; :: thesis: contradiction
exp (b,(b -exponent a)) c= a by A2, A1, ORDINAL5:def 10;
hence contradiction by A3, A5, ORDINAL1:5; :: thesis: verum

end;

hence b -exponent a in c by A4, XBOOLE_0:def 8, ORDINAL1:11; :: thesis: verum