let m be Element of NAT ; :: thesis: for j being Integer st m = j holds
m + 2 = (abs j) + 2
let j be Integer; :: thesis: ( m = j implies m + 2 = (abs j) + 2 )
assume m = j ; :: thesis: m + 2 = (abs j) + 2
then A1: j = m
.= m ;
then j >= 0 by NAT_1:2;
hence (abs j) + 2 = m + 2 by A1, ABSVALUE:def 1
.= m + 2
.= m + 2 ;
:: thesis: verum