defpred S₁[ Nat] means ( 0 <= (2 to_power ($1 -' 1)) - 1 & - (2 to_power ($1 -' 1)) <= 0 );
A1: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

let k be non zero Nat; :: thesis:
assume that
A2: 0 <= (2 to_power (k -' 1)) - 1 and
- (2 to_power (k -' 1)) <= 0 ; :: thesis:
(k + 1) -' 1 = k by NAT_D:34;
then 2 to_power (k -' 1) < 2 to_power ((k + 1) -' 1) by NAT_2:9, POWER:39;
hence S₁[k + 1] by A2, XREAL_1:9; :: thesis:

end;