defpred S₁[ Nat] means for x being Element of F₁() st height x <= $1 holds
P₁[x];
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
for x being Element of F₁() st height x <= n + 1 holds
P₁[x]

proof

let x be Element of F₁(); :: thesis: ( height x <= n + 1 implies P₁[x] )
assume A4: height x <= n + 1 ; :: thesis: P₁[x]

per cases ( height x = n + 1 or P₁[x] ) by A3, A4, NAT_1:8;

suppose A5: height x = n + 1 ; :: thesis: P₁[x]

for y being Element of F₁() st y < x holds
P₁[y]

proof

let y be Element of F₁(); :: thesis: ( y < x implies P₁[y] )
assume y < x ; :: thesis: P₁[y]
then height y < height x by Th2;
then height y <= n by A5, NAT_1:13;
hence P₁[y] by A3; :: thesis: verum

end;

hence P₁[x] by A1; :: thesis: verum

end;

suppose P₁[x] ; :: thesis: P₁[x]

hence P₁[x] ; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] ; :: thesis: verum

end;

let x be Element of F₁(); :: thesis: P₁[x]
A6: ( ( for x being Element of F₁() st height x <= height x holds
P₁[x] ) implies for x being Element of F₁() holds P₁[x] )

proof

assume that
A7: for x being Element of F₁() st height x <= height x holds
P₁[x] and
A8: not for x being Element of F₁() holds P₁[x] ; :: thesis: contradiction
consider x being Element of F₁() such that
A9: P₁[x] by A8;
( height x <= height x implies P₁[x] ) by A7;
hence contradiction by A9; :: thesis: verum

end;

A10: S₁[ 0 ] by Th7;
for n being Nat holds S₁[n] from NAT_1:sch 2(A10, A2);
hence P₁[x] by A6; :: thesis: verum