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 Def5;
A3: now :: thesis: ( B c= C implies C -^ B c= C -^ A )
assume A4: B c= C ; :: thesis: C -^ B c= C -^ A
then A5: C = B +^ (C -^ B) by Def5;
A c= C by A1, A4;
then B +^ (C -^ B) = A +^ (C -^ A) by A5, Def5;
then A +^ ((B -^ A) +^ (C -^ B)) = A +^ (C -^ A) by A2, Th30;
then (B -^ A) +^ (C -^ B) = C -^ A by Th21;
hence C -^ B c= C -^ A by Th24; :: thesis: verum
end;
( not B c= C implies C -^ B c= C -^ A ) by Def5;
hence C -^ B c= C -^ A by A3; :: thesis: verum