take 2 ; :: thesis: not 2 is unit
thus not 2 is unit ; :: thesis: verum