theorem :: LTLAXIO2:33

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