defpred S1[ Nat] means 4 <= Radix $1;
A1: for kk being Nat st kk >= 2 & S1[kk] holds
S1[kk + 1]
proof
let kk be Nat; :: thesis: ( kk >= 2 & S1[kk] implies S1[kk + 1] )
assume that
2 <= kk and
A2: 4 <= Radix kk ; :: thesis: S1[kk + 1]
Radix (kk + 1) = 2 to_power (kk + 1) by RADIX_1:def 1
.= (2 to_power 1) * (2 to_power kk) by POWER:27
.= 2 * (2 to_power kk) by POWER:25
.= 2 * (Radix kk) by RADIX_1:def 1 ;
then Radix (kk + 1) >= Radix kk by XREAL_1:151;
hence S1[kk + 1] by A2, XXREAL_0:2; :: thesis: verum
end;
Radix 2 = 2 to_power (1 + 1) by RADIX_1:def 1
.= (2 to_power 1) * (2 to_power 1) by POWER:27
.= 2 * (2 to_power 1) by POWER:25
.= 2 * 2 by POWER:25 ;
then A3: S1[2] ;
 for i being Nat st 2 <= i holds
S1[i] from NAT_1:sch 8(A3, A1);
 hence for k being Nat st 2 <= k holds
4 <= Radix k ; :: thesis: verum