let A, B, C be Ordinal; :: thesis: ( A c= B implies C -^ B c= C -^ A )
assume A1: A c= B ; :: thesis: C -^ B c= C -^ A
then A2: B = A +^ (B -^ A) by Def6;

A3: now

assume A4: B c= C ; :: thesis: C -^ B c= C -^ A
then A5: C = B +^ (C -^ B) by Def6;
A c= C by A1, A4, XBOOLE_1:1;
then B +^ (C -^ B) = A +^ (C -^ A) by A5, Def6;
then A +^ ((B -^ A) +^ (C -^ B)) = A +^ (C -^ A) by A2, Th33;
then (B -^ A) +^ (C -^ B) = C -^ A by Th24;
hence C -^ B c= C -^ A by Th27; :: thesis: verum

end;

now

assume not B c= C ; :: thesis: C -^ B c= C -^ A
then C -^ B = {} by Def6;
hence C -^ B c= C -^ A by XBOOLE_1:2; :: thesis: verum

end;

hence C -^ B c= C -^ A by A3; :: thesis: verum