len (Cage C,n) > 0 + 1 by GOBOARD7:36, XXREAL_0:2;
then (len (Cage C,n)) - 1 > 0 by XREAL_1:22;
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:36;
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:21;
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; :: thesis: verum