theorem Th44: :: LTLAXIO2:44

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