theorem :: LTLAXIO2:28

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