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