scheme :: NAT_1:sch 18
MinPred{ F1( Nat) -> Nat, P1[ object ] } :
ex k being Nat st
( P1[k] & ( for n being Nat st P1[n] holds
k <= n ) )
provided
A1: for k being Nat holds
( F1((k + 1)) < F1(k) or P1[k] )