defpred S1[ Nat] means for H being ZF-formula st len H = $1 holds
P1[H];
A5: for n being Nat st ( for k being Nat st k < n holds
S1[k] ) holds
S1[n]
proof
let n be Nat; :: thesis: ( ( for k being Nat st k < n holds
S1[k] ) implies S1[n] )
assume A6: for k being Nat st k < n holds
for H being ZF-formula st len H = k holds
P1[H] ; :: thesis: S1[n]
let H be ZF-formula; :: thesis: ( len H = n implies P1[H] )
assume A7: len H = n ; :: thesis: P1[H]
A8: now :: thesis: ( H is conjunctive implies P1[H] )
assume A9: H is conjunctive ; :: thesis: P1[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: P1[ 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 P1[ the_left_argument_of H] by A6, A7;
hence P1[H] by A3, A9, A11; :: thesis: verum
end;
A12: now :: thesis: ( H is universal implies P1[H] )
assume A13: H is universal ; :: thesis: P1[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 P1[H] by A4, A6, A7, A13; :: thesis: verum
end;
now :: thesis: ( H is negative implies P1[H] )
assume A14: H is negative ; :: thesis: P1[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 P1[H] by A2, A6, A7, A14; :: thesis: verum
end;
hence P1[H] by A1, A8, A12, Th10; :: thesis: verum
end;
A15: for n being Nat holds S1[n] from NAT_1:sch 4(A5);
 let H be ZF-formula; :: thesis: P1[H]
len H = len H ;
hence P1[H] by A15; :: thesis: verum