let a, b, c be Ordinal; :: thesis:
assume A1: a c= c ; :: thesis:

suppose A2: ( 1 in b & 0 in a & 0 in c ) ; :: thesis:

then exp (b,(b -exponent a)) c= a by ORDINAL5:def 10;
then exp (b,(b -exponent a)) c= c by A1, XBOOLE_1:1;
hence b -exponent a c= b -exponent c by A2, ORDINAL5:def 10; :: thesis:

end;

suppose not 1 in b ; :: thesis:

then ( b -exponent a = 0 & b -exponent c = 0 ) by ORDINAL5:def 10;
hence b -exponent a c= b -exponent c ; :: thesis:

end;

suppose ( not 0 in a or not 0 in c ) ; :: thesis:

then not 0 in a by A1;
then b -exponent a = {} by ORDINAL5:def 10;
hence b -exponent a c= b -exponent c ; :: thesis:

end;

end;