defpred S₁[ Nat] means 4 <= Radix $1;
A1: for kk being Nat st kk >= 2 & S₁[kk] holds
S₁[kk + 1]

proof

let kk be Nat; :: thesis: ( kk >= 2 & S₁[kk] implies S₁[kk + 1] )
assume that
2 <= kk and
A2: 4 <= Radix kk ; :: thesis: S₁[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 S₁[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: S₁[2] ;
for i being Nat st 2 <= i holds
S₁[i] from NAT_1:sch 8(A3, A1);
hence for k being Nat st 2 <= k holds
4 <= Radix k ; :: thesis: verum