let n, m be Element of NAT ; :: thesis: ( n > 0 implies GBP <> intpos (m + n) )
assume A1: n > 0 ; :: thesis: GBP <> intpos (m + n)
n <= m + n by NAT_1:11;
hence GBP <> intpos (m + n) by A1, AMI_3:52; :: thesis: verum