let i, j be natural Number ; :: thesis: max (0,(i - j)) is Element of NAT
per cases ( i <= j or j <= i ) ;
suppose i <= j ; :: thesis: max (0,(i - j)) is Element of NAT
hence max (0,(i - j)) is Element of NAT by Th2; :: thesis: verum
end;
suppose A1: j <= i ; :: thesis: max (0,(i - j)) is Element of NAT
then i - j is Element of NAT by NAT_1:21;
hence max (0,(i - j)) is Element of NAT by A1, Th3; :: thesis: verum
end;
end;