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;