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

proof

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

end;

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