defpred S1[ Nat] means for m, n being Element of NAT st m <= $1 & n <= $1 holds
P1[m,n];
A3: for k being Nat st ( for r being Nat st r < k holds
S1[r] ) holds
S1[k]
proof
let k be Nat; :: thesis: ( ( for r being Nat st r < k holds
S1[r] ) implies S1[k] )
assume A4: for r being Nat st r < k holds
S1[r] ; :: thesis: S1[k]
let m, n be Element of NAT ; :: thesis: ( m <= k & n <= k implies P1[m,n] )
assume that
A5: m <= k and
A6: n <= k ; :: thesis: P1[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;
per cases ( max (m,n) < k or max (m,n) = k ) by A7, XXREAL_0:1;
suppose max (m,n) < k ; :: thesis: P1[m,n]
then ( m <= max (m,n) & n <= max (m,n) implies P1[m,n] ) by A4, A0;
hence P1[m,n] by XXREAL_0:25; :: thesis: verum
end;
suppose A8: max (m,n) = k ; :: thesis: P1[m,n]
A9: for m, n being Element of NAT st m < k & n < k holds
P1[m,n]
proof
let m, n be Element of NAT ; :: thesis: ( m < k & n < k implies P1[m,n] )
assume that
A10: m < k and
A11: n < k ; :: thesis: P1[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 P1[m,n] by A4, A0, A12, A13; :: thesis: verum
end;
thus P1[m,n] :: thesis: verum
end;
end;
end;
A14: for k being Nat holds S1[k] from NAT_1:sch 4(A3);
 let m, n be Element of NAT ; :: thesis: P1[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 P1[m,n] ) by A14;
hence P1[m,n] by XXREAL_0:30; :: thesis: verum