This rule allows you to introduce an exists formula into your proof from a formula you have already shown (usually containing a closed term you substitute the new exists variable for), or when used backwards allows you get a new goal line from a THERE EXISTS goal line by substituting the variable in it for a closed term (that is already in the box's signature).
To use this rule forwards:

1. select an empty line and click on There Exists Introduction
2. select an formula line in the scope of the empty line containing a non-variable term.
3. then you can either:
   
   1. when prompted enter the formula you want to derive. This will then be checked and added if it can be derived via There Exists Introduction.
      OR
   2. press OK to the first dialogue box that appears (asking you to enter a formula) and enter the term you wish to substitute in the next dialogue followed by the variable name you wish to use.
4. a new THERE EXISTS line will then be added to the proof provided the values you entered in step 3 were valid.

1. select the THERE EXISTS goal line and click on There Exists Introduction.
2. when prompted enter the term you wish to substitute the variable for in the formula, this term must be in the goal line's signature.
3. a new goal line will be added to your proof consisting of the THERE EXISTS formula's sub formula with the variable substituted for the term you entered.