defpred S_{1}[ Nat] means for m, n being Element of NAT st m <= $1 & n <= $1 holds

P_{1}[m,n];

A3: for k being Nat st ( for r being Nat st r < k holds

S_{1}[r] ) holds

S_{1}[k]
_{1}[k]
from NAT_1:sch 4(A3);

let m, n be Element of NAT ; :: thesis: P_{1}[m,n]

set k = max (m,n);

max (m,n) is Nat by TARSKI:1;

then ( m <= max (m,n) & n <= max (m,n) implies P_{1}[m,n] )
by A14;

hence P_{1}[m,n]
by XXREAL_0:30; :: thesis: verum

P

A3: for k being Nat st ( for r being Nat st r < k holds

S

S

proof

A14:
for k being Nat holds S
let k be Nat; :: thesis: ( ( for r being Nat st r < k holds

S_{1}[r] ) implies S_{1}[k] )

assume A4: for r being Nat st r < k holds

S_{1}[r]
; :: thesis: S_{1}[k]

let m, n be Element of NAT ; :: thesis: ( m <= k & n <= k implies P_{1}[m,n] )

assume that

A5: m <= k and

A6: n <= k ; :: thesis: P_{1}[m,n]

set s = max (m,n);

A0: max (m,n) is Nat by TARSKI:1;

A7: max (m,n) <= k by A5, A6, XXREAL_0:28;

end;S

assume A4: for r being Nat st r < k holds

S

let m, n be Element of NAT ; :: thesis: ( m <= k & n <= k implies P

assume that

A5: m <= k and

A6: n <= k ; :: thesis: P

set s = max (m,n);

A0: max (m,n) is Nat by TARSKI:1;

A7: max (m,n) <= k by A5, A6, XXREAL_0:28;

per cases
( max (m,n) < k or max (m,n) = k )
by A7, XXREAL_0:1;

end;

suppose
max (m,n) < k
; :: thesis: P_{1}[m,n]

then
( m <= max (m,n) & n <= max (m,n) implies P_{1}[m,n] )
by A4, A0;

hence P_{1}[m,n]
by XXREAL_0:25; :: thesis: verum

end;hence P

suppose A8:
max (m,n) = k
; :: thesis: P_{1}[m,n]

A9:
for m, n being Element of NAT st m < k & n < k holds

P_{1}[m,n]
_{1}[m,n]
:: thesis: verum

end;P

proof

thus
P
let m, n be Element of NAT ; :: thesis: ( m < k & n < k implies P_{1}[m,n] )

assume that

A10: m < k and

A11: n < k ; :: thesis: P_{1}[m,n]

set s = max (m,n);

A0: max (m,n) is Nat by TARSKI:1;

A12: m <= max (m,n) by XXREAL_0:25;

A13: n <= max (m,n) by XXREAL_0:25;

max (m,n) < k by A10, A11, XXREAL_0:16;

hence P_{1}[m,n]
by A4, A0, A12, A13; :: thesis: verum

end;assume that

A10: m < k and

A11: n < k ; :: thesis: P

set s = max (m,n);

A0: max (m,n) is Nat by TARSKI:1;

A12: m <= max (m,n) by XXREAL_0:25;

A13: n <= max (m,n) by XXREAL_0:25;

max (m,n) < k by A10, A11, XXREAL_0:16;

hence P

let m, n be Element of NAT ; :: thesis: P

set k = max (m,n);

max (m,n) is Nat by TARSKI:1;

then ( m <= max (m,n) & n <= max (m,n) implies P

hence P