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

now :: thesis: ( A <> B implies C +^ A c= C +^ B )

assume A <> B ; :: thesis: C +^ A c= C +^ B
then A c< B by A1, XBOOLE_0:def 8;
then C +^ A in C +^ B by Th32, ORDINAL1:11;
hence C +^ A c= C +^ B by ORDINAL1:def 2; :: thesis: verum

end;

hence C +^ A c= C +^ B ; :: thesis: verum