L1: ( 32 * (t . 1) <= 32 & 16 * (t . 6) <= 16 & 8 * (t . 2) <= 8 & 4 * (t . 3) <= 4 & 2 * (t . 4) <= 2 & 1 * (t . 5) <= 1 ) by CTH1;
then (32 * (t . 1)) + (16 * (t . 6)) <= 32 + 16 by XREAL_1:7;
then ((32 * (t . 1)) + (16 * (t . 6))) + (8 * (t . 2)) <= 48 + 8 by L1, XREAL_1:7;
then (((32 * (t . 1)) + (16 * (t . 6))) + (8 * (t . 2))) + (4 * (t . 3)) <= 56 + 4 by L1, XREAL_1:7;
then ((((32 * (t . 1)) + (16 * (t . 6))) + (8 * (t . 2))) + (4 * (t . 3))) + (2 * (t . 4)) <= 60 + 2 by L1, XREAL_1:7;
then (((((32 * (t . 1)) + (16 * (t . 6))) + (8 * (t . 2))) + (4 * (t . 3))) + (2 * (t . 4))) + (1 * (t . 5)) <= 62 + 1 by L1, XREAL_1:7;
then (((((32 * (t . 1)) + (16 * (t . 6))) + (8 * (t . 2))) + (4 * (t . 3))) + (2 * (t . 4))) + (1 * (t . 5)) < 63 + 1 by XREAL_1:145;
hence (((((32 * (t . 1)) + (16 * (t . 6))) + (8 * (t . 2))) + (4 * (t . 3))) + (2 * (t . 4))) + (1 * (t . 5)) is Element of 64 by NAT_1:44; :: thesis: verum