let a, b be Cardinal; :: thesis: ( a in b +` 1 implies a c= b )
assume A1: a in b +` 1 ; :: thesis: a c= b

per cases ( b is infinite or b is finite ) ;

suppose A2: b is infinite ; :: thesis: a c= b

then 1 c= b ;
then b +` 1 = b by A2, CARD_2:76;
hence a c= b by A1, ORDINAL1:def 2; :: thesis: verum

end;

suppose A3: b is finite ; :: thesis: a c= b

then reconsider m = b as Nat ;
( b +` 1 is finite & a c= b +` 1 ) by A1, A3, ORDINAL1:def 2;
then reconsider n = a as Nat ;
a in Segm (m +` 1) by A1;
then n < m + 1 by NAT_1:44;
then n <= m by NAT_1:13;
then Segm n c= Segm m by NAT_1:39;
hence a c= b ; :: thesis: verum

end;

end;