take 1 / 2 ; :: thesis: not 1 / 2 is integer
thus not 1 / 2 is integer ; :: thesis: verum