take TheNorSymbOf S ; :: thesis: not TheNorSymbOf S is literal
thus not TheNorSymbOf S is literal ; :: thesis: verum