let m, n be Nat; :: thesis: ( n > 1 implies SBP <> intpos (m + n) )
assume A1: n > 1 ; :: thesis: SBP <> intpos (m + n)
n <= m + n by NAT_1:11;
hence SBP <> intpos (m + n) by A1, AMI_3:10; :: thesis: verum