 The fundamental notion of making a supposition (= assumption) and seeing where it leads is indicated in Jaśkowski’s by the introduction of a box, the first line of which is the supposition and all the consequences of that assumption are retained inside that box. Moreover, further suppositions can be made within the previous box by generating a subordinate box. The fundamental rule of Conditionalization is that a conditional whose antecedent is the supposition and whose consequent is the final line inside the box can be entered as the next line outside the box. Once a box has been constructed, no formula within it can be used to justify any line of the proof outside of the box. A similar rule of supposition is the Reductio, or Negation Introduction, rule, where two contradictory lines inside the same box can trigger a completion (closing) of the box and the unnegated supposition as the next line outside the box. A theorem of the language is a formula that can be generated by these rules and is outside of all boxes. As with the Gentzen proof, we see that Jaśkowski’s use of the rule Reductio ad Absurdum deletes a negation sign from the assumption. This is Jaśkowski’s way to move from intuitionistic logic to classical logic. (Again, see  note 23  for methods of strengthening intuitionistic logic to classical logic.)