let a, b be Ordinal; :: thesis: ( a in b implies b -exponent a = 0 )
assume A1: a in b ; :: thesis: b -exponent a = 0
per cases ( 0 in a or not 0 in a ) ;
suppose 0 in a ; :: thesis: b -exponent a = 0
then 0 = b -exponent (a *^ (exp (b,0))) by A1, ORDINAL5:58
.= b -exponent (a *^ 1) by ORDINAL2:43
.= b -exponent a by ORDINAL2:39 ;
hence b -exponent a = 0 ; :: thesis: verum
end;
suppose not 0 in a ; :: thesis: b -exponent a = 0
hence b -exponent a = 0 by ORDINAL5:def 10; :: thesis: verum
end;
end;