defpred S₁[ 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 S₁[n] by A1;
consider IT being Nat such that
A3: ( S₁[IT] & ( for n being Nat st S₁[n] holds
IT <= n ) ) from NAT_1:sch 5(A2);
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 A3; :: thesis: verum