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