defpred S_{1}[ 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_{1}[n]
by A1;

consider IT being Nat such that

A3: ( S_{1}[IT] & ( for n being Nat st S_{1}[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

consider m being Nat such that

A1: phi is m -wff by Def24;

A2: ex n being Nat st S

consider IT being Nat such that

A3: ( S

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