let n, m be Element of NAT ; :: thesis: ( prop n = prop m implies n = m )
assume prop n = prop m ; :: thesis: n = m
then 3 + n = 3 + m by GROUP_7:1;
hence n = m ; :: thesis: verum