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

A2: now :: thesis: ( C c= A implies A -^ C c= B -^ C )

assume A3: C c= A ; :: thesis: A -^ C c= B -^ C
then A4: A = C +^ (A -^ C) by Def5;
C c= B by A1, A3;
then C +^ (A -^ C) c= C +^ (B -^ C) by A1, A4, Def5;
hence A -^ C c= B -^ C by Th23; :: thesis: verum

end;

( not C c= A implies A -^ C c= B -^ C ) by Def5;
hence A -^ C c= B -^ C by A2; :: thesis: verum