theorem Th34: :: LTLAXIO1:34

for p, q being Element of LTLB_WFF holds p => (q => p) in LTL_axioms