theorem :: ZF_LANG1:10

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