defpred S₁[ Nat] means for m, n being Nat st m <= $1 & n <= $1 holds
P₁[m,n];
A3: for k being Nat st ( for r being Nat st r < k holds
S₁[r] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( ( for r being Nat st r < k holds
S₁[r] ) implies S₁[k] )
assume A4: for r being Nat st r < k holds
S₁[r] ; :: thesis: S₁[k]
let m, n be Nat; :: thesis: ( m <= k & n <= k implies P₁[m,n] )
assume that
A5: m <= k and
A6: n <= k ; :: thesis: P₁[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: P₁[m,n]

then ( m <= max (m,n) & n <= max (m,n) implies P₁[m,n] ) by A4, A0;
hence P₁[m,n] by XXREAL_0:25; :: thesis: verum

end;

suppose A8: max (m,n) = k ; :: thesis: P₁[m,n]

A9: for m, n being Nat st m < k & n < k holds
P₁[m,n]

proof

let m, n be Nat; :: thesis: ( m < k & n < k implies P₁[m,n] )
assume that
A10: m < k and
A11: n < k ; :: thesis: P₁[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₁[m,n] by A4, A0, A12, A13; :: thesis: verum

end;

thus P₁[m,n] :: thesis: verum

proof

per cases ( k = m or k = n ) by A8, XXREAL_0:16;

suppose k = m ; :: thesis: P₁[m,n]

hence P₁[m,n] by A2, A6, A9; :: thesis: verum

end;

suppose k = n ; :: thesis: P₁[m,n]

then P₁[n,m] by A2, A5, A9;
hence P₁[m,n] by A1; :: thesis: verum

end;

end;

end;

end;

end;

end;

A14: for k being Nat holds S₁[k] from NAT_1:sch 4(A3);
let m, n be Nat; :: thesis: P₁[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₁[m,n] ) by A14;
hence P₁[m,n] by XXREAL_0:30; :: thesis: verum