theorem Th52: :: LTLAXIO1:52

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