let A, B be Ordinal; :: thesis: ( A c= B implies B = A +^ (B -^ A) )
assume A1: A c= B ; :: thesis: B = A +^ (B -^ A)

per cases ( A = B or A <> B ) ;

suppose A2: A = B ; :: thesis: B = A +^ (B -^ A)

then B -^ A = 0 by ORDINAL3:54;
hence B = A +^ (B -^ A) by A2, ORDINAL2:27; :: thesis: verum

end;

suppose A <> B ; :: thesis: B = A +^ (B -^ A)

then A c< B by A1;
hence B = A +^ (B -^ A) by ORDINAL1:11, ORDINAL3:51; :: thesis: verum

end;

end;