This rule can be used forwards to derive anything from a false formula or backwards to produce a bottom formula from which the goal line was derived.
To use it forwards:

1. select an empty line and click on Bottom Elimination.
2. then select the bottom line you wish to use for the rule (the formula must be in the scope of the empty line).
3. when prompted, enter the formula you wish to derive. This formula must not contain any predicate symbols, function symbols or constants that are not in the signature of the box you are working in.
4. if the formula you entered was valid it will appear as a new line in your proof.

1. select a goal line to be derived from bottom and click on Bottom Elimination.
2. a new bottom goal line will be added to your proof.