:: deftheorem Def10 defines -exponent ORDINAL5:def 10 :
for a, b, b₃ being Ordinal holds
( ( 1 in b & 0 in a implies ( b₃ = b -exponent a iff ( exp (b,b₃) c= a & ( for c being Ordinal st exp (b,c) c= a holds
c c= b₃ ) ) ) ) & ( ( not 1 in b or not 0 in a ) implies ( b₃ = b -exponent a iff b₃ = 0 ) ) );