Changed definition of permissionDenied and permissionDenied
to make them simpler.

Proved a few auxilary theorems and finally proved theo10.