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