[Logiweb] rule

[Martin Røpcke]

If I would like to state a rule and use it in another proof how do I do 
this? I remember that either Klaus said something about it or I have read 
about it somewhere. I tried with:

"[math in theory system prime s
 	rule mendelson proposition three two h g ii
 	says
 	.
 	.
 	.
 	end rule
end math ]"

But I get an error saying "the theory does not assert this rule". I can 
state it as a lemma, and I'm pretty sure it's valid, though I havn't 
proved it yet. The lemma/rule is:

x' + y = (x + y)' |- y' + x = (y + x)'

I believe this should be provable.

Regards,
Martin