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