The Direct command can only be used when you
have a goal of the form P
Q.
If you select a goal of
this form and give the Direct command, then Proof Designer will create a
subproof in which it is assumed that P is true, and it will say
that to complete the subproof you must prove Q.