take a = - (1 / 2); :: thesis: ( a is negative & not a is integer )
thus ( a is negative & not a is integer ) by ThA; :: thesis: verum