theorem Th50: :: LTLAXIO1:50

for p, q, r, s being Element of LTLB_WFF
for X being Subset of LTLB_WFF st X |- (p '&&' q) => r & X |- p => s holds
X |- (p '&&' q) => (s '&&' r)