let k be Integer; :: thesis: (30 * k) + 7 is odd
A1: 30 * k = 2 * (15 * k) ;
7 = (3 * 2) + 1 ;
hence (30 * k) + 7 is odd by A1; :: thesis: verum