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

assume C c= A ; :: thesis: A -^ C c= B -^ C
then ( C c= B & A = C +^ (A -^ C) ) by A1, Def6, XBOOLE_1:1;
then C +^ (A -^ C) c= C +^ (B -^ C) by A1, Def6;
hence A -^ C c= B -^ C by Th26; :: thesis: verum

end;

now

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

end;

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