defpred S1[ Nat] means phi is $1 -wff ;
consider m being Nat such that
A1:
phi is m -wff
by Def24;
A2:
ex n being Nat st S1[n]
by A1;
consider IT being Nat such that
A3:
( S1[IT] & ( for n being Nat st S1[n] holds
IT <= n ) )
from NAT_1:sch 5(A2);
take
IT
; ( phi is IT -wff & ( for n being Nat st phi is n -wff holds
IT <= n ) )
thus
( phi is IT -wff & ( for n being Nat st phi is n -wff holds
IT <= n ) )
by A3; verum