defpred S₁[ Nat] means 2 <= Radix $1;
let k be Nat; :: thesis: ( 1 <= k implies 2 <= Radix k )
assume A1: 1 <= k ; :: thesis: 2 <= Radix k
A2: for kk being Nat st kk >= 1 & S₁[kk] holds
S₁[kk + 1]

proof

let kk be Nat; :: thesis: ( kk >= 1 & S₁[kk] implies S₁[kk + 1] )
assume that
1 <= kk and
A3: 2 <= Radix kk ; :: thesis: S₁[kk + 1]
A4: Radix (kk + 1) = (2 to_power 1) * (2 to_power kk) by POWER:27
.= 2 * (Radix kk) by POWER:25 ;
Radix kk > 1 by A3, XXREAL_0:2;
hence S₁[kk + 1] by A4, XREAL_1:155; :: thesis: verum

end;

A5: S₁[1] by POWER:25;
for k being Nat st 1 <= k holds
S₁[k] from NAT_1:sch 8(A5, A2);
hence 2 <= Radix k by A1; :: thesis: verum