theorem Th48: :: LTLAXIO2:48

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