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