let m be Nat; :: thesis: m = abs m
m >= 0 by NAT_1:2;
hence abs m = m by Def1; :: thesis: verum