theorem :: LTLAXIO2:36

for p, q being Element of LTLB_WFF holds ('not' (p 'or' q)) => (('not' p) '&&' ('not' q)) is ctaut