let A be non empty set ; :: thesis: for v being Element of Valuations_in A
for p being Element of CQC-WFF
for J being interpretation of A holds (Valid ('not' (p '&' ('not' p))),J) . v = TRUE
let v be Element of Valuations_in A; :: thesis: for p being Element of CQC-WFF
for J being interpretation of A holds (Valid ('not' (p '&' ('not' p))),J) . v = TRUE
let p be Element of CQC-WFF ; :: thesis: for J being interpretation of A holds (Valid ('not' (p '&' ('not' p))),J) . v = TRUE
let J be interpretation of A; :: thesis: (Valid ('not' (p '&' ('not' p))),J) . v = TRUE
(Valid ('not' (p '&' ('not' p))),J) . v = 'not' ((Valid (p '&' ('not' p)),J) . v) by Th20
.= 'not' FALSE by Th24 ;
hence (Valid ('not' (p '&' ('not' p))),J) . v = TRUE by MARGREL1:41; :: thesis: verum