theorem naab: :: PL_AXIOM:60

for A, B being Element of PL-WFF
for F being Subset of PL-WFF holds F |- ('not' A) => (A => B)