theorem Th12: :: LTLAXIO3:12

for p being Element of LTLB_WFF holds tau1 . p c= tau1 . ('not' p)