for p being MP-variable
for A, B being MP-wff holds
( @ p <> 'not' A & @ p <> (#) A & @ p <> A '&' B )