len (Cage (C,n)) > 0 + 1
by GOBOARD7:34, XXREAL_0:2;
then
(len (Cage (C,n))) - 1 > 0
by XREAL_1:20;
then A1:
(len (Cage (C,n))) -' 1 = (len (Cage (C,n))) - 1
by XREAL_0:def 2;
A2:
len (Cage (C,n)) > 4
by GOBOARD7:34;
len (Cage (C,n)) < (len (Cage (C,n))) + 1
by NAT_1:13;
then
(len (Cage (C,n))) -' 1 < len (Cage (C,n))
by A1, XREAL_1:19;
then A3:
(Cage (C,n)) | ((len (Cage (C,n))) -' 1) is one-to-one
by A2, TOPREAL8:22;
(Cage (C,n)) /^ 1 is one-to-one
;
hence
Cage (C,n) is almost-one-to-one
by A3, Th14; verum