theorem :: LTLAXIO2:27

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