defpred S₁[ Nat] means Radix $1 >= 2 + 2;
let k be Nat; :: thesis: ( k >= 2 implies Radix k >= 2 + 2 )
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 kk >= 2 ; :: thesis: ( not S₁[kk] or S₁[kk + 1] )
Radix (kk + 1) = (2 to_power kk) * (2 to_power 1) by POWER:27
.= (Radix kk) * 2 ;
then A2: Radix (kk + 1) >= Radix kk by XREAL_1:155;
assume Radix kk >= 2 + 2 ; :: thesis: S₁[kk + 1]
hence S₁[kk + 1] by A2, XXREAL_0:2; :: thesis: verum

end;

Radix 2 = 2 to_power (1 + 1)
.= (2 to_power 1) * (2 to_power 1) by POWER:27
.= 2 * (2 to_power 1)
.= 2 * 2 ;
then A3: S₁[2] ;
for k being Nat st k >= 2 holds
S₁[k] from NAT_1:sch 8(A3, A1);
hence ( k >= 2 implies Radix k >= 2 + 2 ) ; :: thesis: verum