With claim (a) disposed of, consider again claim (b) that, while not all diagrammatic thinking in a process of thinking through a proof is superfluous, all non-superfluous diagrammatic thinking will be replaceable by non-diagrammatic thinking in a process of thinking through that same proof. The visual thinking in following the proof of Euclid’s first theorem using Miller’s formal system consists in going through a sequence of diagrams and at each step seeing that the next diagram results from a permitted alteration of the previous diagram. It is clear that in a process that counts as thinking through this proof, the diagrammatic thinking is neither superfluous nor replaceable by non-diagrammatic thinking. That knocks out (b), leaving only (c): some thinking that involves a diagram in thinking through a proof is neither superfluous nor replaceable by non-diagrammatic thinking (without changing the proof).