let k be Nat; :: thesis: ( 2 <= k implies 2 < Radix k )
defpred S₁[ Nat] means 2 < 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: 2 < Radix kk ; :: thesis: S₁[kk + 1]
A3: Radix (kk + 1) = (2 to_power 1) * (2 to_power kk) by POWER:27
.= 2 * (Radix kk) by POWER:25 ;
Radix kk > 1 by A2, XXREAL_0:2;
hence S₁[kk + 1] by A3, XREAL_1:155; :: 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) by POWER:25
.= 2 * 2 by POWER:25
.= 4 ;
then A4: S₁[2] ;
for k being Nat st 2 <= k holds
S₁[k] from NAT_1:sch 8(A4, A1);
hence ( 2 <= k implies 2 < Radix k ) ; :: thesis: verum