Use the Contradiction command if you want to do a proof by contradiction. Select the goal that you want to prove by contradiction and give the Contradiction command. Proof Designer will create a subproof in which it is assumed that the goal is false, and then it will say that you must prove a contradiction to complete the subproof. The negation of the original goal will be added to the givens list, and the new goal will be listed as “Contradiction”.
If you are working on a proof by contradiction and you think you know which given you want to contradict, you can select it and give the Contradiction command. Proof Designer will indicate that you have to prove the negation of the selected given in order to arrive at the desired contradiction.
You can combine these two uses of the Contradiction command in one step: If you want to do a proof by contradiction and you know right from the start which given you want to contradict, select the given and give the Contradiction command. Proof Designer will create a subproof in which it is assumed that the goal is false, and then it will say that you must prove the negation of the selected given to arrive at a contradiction.