for p, q being ZF-formula holds p 'or' q = ('not' p) => q ;