theorem Th34: :: LTLAXIO2:34

for p, q being Element of LTLB_WFF holds p => (q => (p => q)) is ctaut