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 J,v |= (('not' p) => p) => p
let v be Element of Valuations_in A; :: thesis: for p being Element of CQC-WFF
for J being interpretation of A holds J,v |= (('not' p) => p) => p
let p be Element of CQC-WFF ; :: thesis: for J being interpretation of A holds J,v |= (('not' p) => p) => p
let J be interpretation of A; :: thesis: J,v |= (('not' p) => p) => p
thus (Valid ((('not' p) => p) => p),J) . v = TRUE :: according to VALUAT_1:def 12 :: thesis: verum

proof

('not' p) => p = 'not' (('not' p) '&' ('not' p)) by QC_LANG2:def 2;
then A1: (Valid ((('not' p) => p) => p),J) . v = (Valid ('not' (('not' (('not' p) '&' ('not' p))) '&' ('not' p))),J) . v by QC_LANG2:def 2
.= 'not' ((Valid (('not' (('not' p) '&' ('not' p))) '&' ('not' p)),J) . v) by Th20
.= 'not' (((Valid ('not' (('not' p) '&' ('not' p))),J) . v) '&' ((Valid ('not' p),J) . v)) by Th22 ;
(Valid ('not' (('not' p) '&' ('not' p))),J) . v = 'not' ((Valid (('not' p) '&' ('not' p)),J) . v) by Th20
.= 'not' ((Valid ('not' p),J) . v) by Th33
.= 'not' ('not' ((Valid p,J) . v)) by Th20
.= (Valid p,J) . v ;
hence (Valid ((('not' p) => p) => p),J) . v = 'not' (((Valid p,J) . v) '&' ('not' ((Valid p,J) . v))) by A1, Th20
.= TRUE by XBOOLEAN:102 ;
:: thesis: verum

end;