defpred S1[ Nat] means for x being Element of F1() st height x <= $1 holds
P1[x];
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; :: thesis: S1[n + 1]
for x being Element of F1() st height x <= n + 1 holds
P1[x]
proof
let x be Element of F1(); :: thesis: ( height x <= n + 1 implies P1[x] )
assume A4: height x <= n + 1 ; :: thesis: P1[x]
per cases ( height x = n + 1 or P1[x] ) by A3, A4, NAT_1:8;
suppose A5: height x = n + 1 ; :: thesis: P1[x]
for y being Element of F1() st y < x holds
P1[y]
proof
let y be Element of F1(); :: thesis: ( y < x implies P1[y] )
assume y < x ; :: thesis: P1[y]
then height y < height x by Th2;
then height y <= n by A5, NAT_1:13;
hence P1[y] by A3; :: thesis: verum
end;
hence P1[x] by A1; :: thesis: verum
end;
end;
end;
hence S1[n + 1] ; :: thesis: verum
end;
let x be Element of F1(); :: thesis: P1[x]
A6: ( ( for x being Element of F1() st height x <= height x holds
P1[x] ) implies for x being Element of F1() holds P1[x] )
proof
assume that
A7: for x being Element of F1() st height x <= height x holds
P1[x] and
A8: not for x being Element of F1() holds P1[x] ; :: thesis: contradiction
consider x being Element of F1() such that
A9: P1[x] by A8;
( height x <= height x implies P1[x] ) by A7;
hence contradiction by A9; :: thesis: verum
end;
A10: S1[ 0 ] by Th7;
for n being Nat holds S1[n] from NAT_1:sch 2(A10, A2);
 hence P1[x] by A6; :: thesis: verum