theorem Th36: :: VALUAT_1:36

for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q, t being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))