 Sets like \(B\) and \(B′\) are called bars. Brouwer first formulates a condition for any demonstration that may be found of the proposition “Tree \(T\) contains a bar”. This condition is that any demonstration of that proposition must be analyzable into a certain canonical form. Brouwer then gives a method to transform any such demonstration, when analyzed into that canonical form, into a mathematical construction that makes the proposition “\(T\) contains a well-ordered bar”, true, thereby establishing the consequent. This strategy clearly shows that Brouwer’s operative explanation of the meaning of \(A \rightarrow B\) was a version of clause (H3) of the Proof Interpretation as formulated in the Introduction, if we understand “proof” in that clause as “demonstration”.