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;