defpred S₁[ Nat] means phi is $1 -wff ;
consider m being Nat such that
B0: phi is m -wff by DefWff2;
B1: ex n being Nat st S₁[n] by B0;
consider IT being Nat such that
B2: ( S₁[IT] & ( for n being Nat st S₁[n] holds
IT <= n ) ) from NAT_1:sch 5(B1);
take IT ; :: thesis: ( 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 B2; :: thesis: verum