let A be non empty set ; :: thesis: for v being Element of Valuations_in A
for p, q being Element of CQC-WFF
for J being interpretation of A holds J,v |= p => (('not' p) => q)
let v be Element of Valuations_in A; :: thesis: for p, q being Element of CQC-WFF
for J being interpretation of A holds J,v |= p => (('not' p) => q)
let p, q be Element of CQC-WFF ; :: thesis: for J being interpretation of A holds J,v |= p => (('not' p) => q)
let J be interpretation of A; :: thesis: J,v |= p => (('not' p) => q)
thus
(Valid (p => (('not' p) => q)),J) . v = TRUE
:: according to VALUAT_1:def 12 :: thesis: verumproof
('not' p) => q = 'not' (('not' p) '&' ('not' q))
by QC_LANG2:def 2;
then A1:
(Valid (p => (('not' p) => q)),J) . v =
(Valid ('not' (p '&' ('not' ('not' (('not' p) '&' ('not' q)))))),J) . v
by QC_LANG2:def 2
.=
'not' ((Valid (p '&' ('not' ('not' (('not' p) '&' ('not' q))))),J) . v)
by Th20
.=
'not' (((Valid p,J) . v) '&' ((Valid ('not' ('not' (('not' p) '&' ('not' q)))),J) . v))
by Th22
;
(Valid ('not' ('not' (('not' p) '&' ('not' q)))),J) . v =
'not' ((Valid ('not' (('not' p) '&' ('not' q))),J) . v)
by Th20
.=
'not' ('not' ((Valid (('not' p) '&' ('not' q)),J) . v))
by Th20
.=
((Valid ('not' p),J) . v) '&' ((Valid ('not' q),J) . v)
by Th22
.=
('not' ((Valid p,J) . v)) '&' ((Valid ('not' q),J) . v)
by Th20
.=
('not' ((Valid p,J) . v)) '&' ('not' ((Valid q,J) . v))
by Th20
;
then A2:
(Valid (p => (('not' p) => q)),J) . v =
'not' ((((Valid p,J) . v) '&' ('not' ((Valid p,J) . v))) '&' ('not' ((Valid q,J) . v)))
by A1, MARGREL1:52
.=
'not' (FALSE '&' ('not' ((Valid q,J) . v)))
by XBOOLEAN:138
;
FALSE '&' ('not' ((Valid q,J) . v)) = FALSE
by MARGREL1:49;
hence
(Valid (p => (('not' p) => q)),J) . v = TRUE
by A2, MARGREL1:41;
:: thesis: verum
end;