let a, b, c be Cardinal; :: thesis: ( a c= c & b c= c & c c< a +` 2 & not b c= a implies b = c )
assume A1: ( a c= c & b c= c & c c< a +` 2 & not b c= a ) ; :: thesis: b = c
A2: c is finite

proof

assume c is infinite ; :: thesis: contradiction
then A3: a is infinite by A1, XBOOLE_0:def 8, FINSET_1:1;
then 2 c= a ;
then a +` 2 = a by A3, CARD_2:76;
then c in a by A1, ORDINAL1:11;
then c in c by A1;
hence contradiction ; :: thesis: verum

end;

then reconsider n = c as Nat ;
reconsider k = a as Nat by A1, A2;
A4: a in b by A1, ORDINAL1:16;
reconsider m = b as Nat by A1, A2;
Segm b c= Segm c by A1;
then A5: m <= n by NAT_1:39;
c in Segm (k +` 2) by A1, ORDINAL1:11;
then A6: n < k + 2 by NAT_1:44;
a in Segm b by A4;
then k < m by NAT_1:44;
then A7: k + 1 <= m by NAT_1:13;
n < (k + 1) + 1 by A6;
then n <= k + 1 by NAT_1:13;
then n <= m by A7, XXREAL_0:2;
hence b = c by A5, XXREAL_0:1; :: thesis: verum