defpred S_{1}[ Nat] means for x being Element of F_{1}() st height x <= $1 holds

P_{1}[x];

A2: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}(); :: thesis: P_{1}[x]

A6: ( ( for x being Element of F_{1}() st height x <= height x holds

P_{1}[x] ) implies for x being Element of F_{1}() holds P_{1}[x] )
_{1}[ 0 ]
by Th7;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A10, A2);

hence P_{1}[x]
by A6; :: thesis: verum

P

A2: for n being Nat st S

S

proof

let x be Element of F
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A3: S_{1}[n]
; :: thesis: S_{1}[n + 1]

for x being Element of F_{1}() st height x <= n + 1 holds

P_{1}[x]
_{1}[n + 1]
; :: thesis: verum

end;assume A3: S

for x being Element of F

P

proof

hence
S
let x be Element of F_{1}(); :: thesis: ( height x <= n + 1 implies P_{1}[x] )

assume A4: height x <= n + 1 ; :: thesis: P_{1}[x]

end;assume A4: height x <= n + 1 ; :: thesis: P

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

end;

suppose A5:
height x = n + 1
; :: thesis: P_{1}[x]

for y being Element of F_{1}() st y < x holds

P_{1}[y]
_{1}[x]
by A1; :: thesis: verum

end;P

proof

hence
P
let y be Element of F_{1}(); :: thesis: ( y < x implies P_{1}[y] )

assume y < x ; :: thesis: P_{1}[y]

then height y < height x by Th2;

then height y <= n by A5, NAT_1:13;

hence P_{1}[y]
by A3; :: thesis: verum

end;assume y < x ; :: thesis: P

then height y < height x by Th2;

then height y <= n by A5, NAT_1:13;

hence P

A6: ( ( for x being Element of F

P

proof

A10:
S
assume that

A7: for x being Element of F_{1}() st height x <= height x holds

P_{1}[x]
and

A8: not for x being Element of F_{1}() holds P_{1}[x]
; :: thesis: contradiction

consider x being Element of F_{1}() such that

A9: P_{1}[x]
by A8;

( height x <= height x implies P_{1}[x] )
by A7;

hence contradiction by A9; :: thesis: verum

end;A7: for x being Element of F

P

A8: not for x being Element of F

consider x being Element of F

A9: P

( height x <= height x implies P

hence contradiction by A9; :: thesis: verum

for n being Nat holds S

hence P