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