This rule can be used forwards to introduce a formula of the form A | ~A into your proof or backwards to justify a line of the form A | ~A.
To use it forwards:

1. select an empty line and click on Law of Excluded Middle.
2. when prompted enter the formula you wish to represent A in A | ~A. This formula must only contain predicate symbols, function symbols or constants in the empty line's signature.
3. the formula a | ~a will then be added to your proof where a is the formula you entered.

1. select a goal line of the form a | ~a and click on Law of Excluded Middle.
2. the formula will then be justified and the box containing the line will be closed (the empty line is removed and the box will turn grey).