defpred S₁[ Nat] means for H being ZF-formula st len H = $1 holds
P₁[H];
A5: for n being Nat st ( for k being Nat st k < n holds
S₁[k] ) holds
S₁[n]

proof

let n be Nat; :: thesis: ( ( for k being Nat st k < n holds
S₁[k] ) implies S₁[n] )
assume A6: for k being Nat st k < n holds
for H being ZF-formula st len H = k holds
P₁[H] ; :: thesis: S₁[n]
let H be ZF-formula; :: thesis: ( len H = n implies P₁[H] )
assume A7: len H = n ; :: thesis: P₁[H]

A8: now :: thesis: ( H is conjunctive implies P₁[H] )

assume A9: H is conjunctive ; :: thesis: P₁[H]
then A10: H = (the_left_argument_of H) '&' (the_right_argument_of H) by Th40;
then the_right_argument_of H is_immediate_constituent_of H ;
then len (the_right_argument_of H) < len H by Th60;
then A11: P₁[ the_right_argument_of H] by A6, A7;
the_left_argument_of H is_immediate_constituent_of H by A10;
then len (the_left_argument_of H) < len H by Th60;
then P₁[ the_left_argument_of H] by A6, A7;
hence P₁[H] by A3, A9, A11; :: thesis: verum

end;

A12: now :: thesis: ( H is universal implies P₁[H] )

assume A13: H is universal ; :: thesis: P₁[H]
then H = All ((bound_in H),(the_scope_of H)) by Th44;
then the_scope_of H is_immediate_constituent_of H ;
then len (the_scope_of H) < len H by Th60;
hence P₁[H] by A4, A6, A7, A13; :: thesis: verum

end;

now :: thesis: ( H is negative implies P₁[H] )

assume A14: H is negative ; :: thesis: P₁[H]
then H = 'not' (the_argument_of H) by Def30;
then the_argument_of H is_immediate_constituent_of H ;
then len (the_argument_of H) < len H by Th60;
hence P₁[H] by A2, A6, A7, A14; :: thesis: verum

end;

hence P₁[H] by A1, A8, A12, Th10; :: thesis: verum

end;

A15: for n being Nat holds S₁[n] from NAT_1:sch 4(A5);
let H be ZF-formula; :: thesis: P₁[H]
len H = len H ;
hence P₁[H] by A15; :: thesis: verum