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; :: thesis: verum