theorem Th35: :: LTLAXIO2:35

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