defpred S₁[ Nat] means P₁[$1];
assume A2: for k being Nat holds
( not P₁[k] or ex n being Nat st
( P₁[n] & not k <= n ) ) ; :: thesis:
A3: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

let k be Nat; :: thesis:
assume A4: for n being Nat st n < k holds
not P₁[n] ; :: thesis:
( ( for n being Nat holds
( not P₁[n] or k <= n ) ) implies not P₁[k] ) by A2;
hence S₁[k] by A4; :: thesis:

end;