let a, b, c be Ordinal; :: thesis: ( b c= c implies a (+) b c= a (+) c )
assume A1: b c= c ; :: thesis: a (+) b c= a (+) c

per cases ( c c= b or b in c ) by ORDINAL1:16;

suppose c c= b ; :: thesis: a (+) b c= a (+) c

hence a (+) b c= a (+) c by A1, XBOOLE_0:def 10; :: thesis: verum

end;

suppose b in c ; :: thesis: a (+) b c= a (+) c

hence a (+) b c= a (+) c by Th107, ORDINAL1:def 2; :: thesis: verum

end;

end;