let a, b be Cardinal; :: thesis: ( a c= b & a <> b implies a +` 1 c= b )
assume A1: ( a c= b & a <> b ) ; :: thesis: a +` 1 c= b
then a c< b by XBOOLE_0:def 8;
then A2: succ a c= b by ORDINAL1:11, ORDINAL1:21;
per cases ( a is finite or a is infinite ) ;
suppose a is finite ; :: thesis: a +` 1 c= b
then reconsider n = a as Nat ;
a +` 1 = n +` 1
.= Segm (n + 1)
.= succ (Segm n) by NAT_1:38
.= succ a ;
hence a +` 1 c= b by A2; :: thesis: verum
end;
suppose A3: a is infinite ; :: thesis: a +` 1 c= b
then 1 c= a ;
hence a +` 1 c= b by A1, A3, CARD_2:76; :: thesis: verum
end;
end;