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;