let n be non zero Element of NAT ; :: thesis: (n -' 1) + 2 = n + 1
n >= 1 by NAT_2:19;
then (n -' 1) + 2 = (n + 2) -' 1 by NAT_D:38
.= (n + 2) - 1 by NAT_D:37 ;
hence (n -' 1) + 2 = n + 1 ; :: thesis: verum