Top Introduction
   
 

This rule is used forwards to introduce a new occurance of the "Top" (T) formula, or backwards to immediately justify a "Top" goal.
To use it forwards:

  1. select an empty line and select Top Introduction from the Apply menu.
  2. a "Top" (T) formula will then be added as a new line to your proof.
To use it backwards:
  1. select the "Top" (T) goal line you wish to justify and select Top Introduction from the Apply menu.
  2. the goal line will then be justified closing the box it is in (the empty line is removed and the box will turn grey).