let A be non empty set ; :: thesis: for p being Element of CQC-WFF
for J being interpretation of A holds Valid ('not' ('not' p)),J = Valid p,J
let p be Element of CQC-WFF ; :: thesis: for J being interpretation of A holds Valid ('not' ('not' p)),J = Valid p,J
let J be interpretation of A; :: thesis: Valid ('not' ('not' p)),J = Valid p,J

now

let v be Element of Valuations_in A; :: thesis: (Valid ('not' ('not' p)),J) . v = (Valid p,J) . v
thus (Valid ('not' ('not' p)),J) . v = 'not' ((Valid ('not' p),J) . v) by Th20
.= 'not' ('not' ((Valid p,J) . v)) by Th20
.= (Valid p,J) . v ; :: thesis: verum

end;

hence Valid ('not' ('not' p)),J = Valid p,J by FUNCT_2:113; :: thesis: verum