theorem :: LTLAXIO2:55

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