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 '&' q) => (q '&' p)
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 '&' q) => (q '&' p)
let p, q be Element of CQC-WFF ; :: thesis: for J being interpretation of A holds J,v |= (p '&' q) => (q '&' p)
let J be interpretation of A; :: thesis: J,v |= (p '&' q) => (q '&' p)
thus
(Valid ((p '&' q) => (q '&' p)),J) . v = TRUE
:: according to VALUAT_1:def 12 :: thesis: verumproof
assume
not
(Valid ((p '&' q) => (q '&' p)),J) . v = TRUE
;
:: thesis: contradiction
then A1:
(Valid ((p '&' q) => (q '&' p)),J) . v = FALSE
by XBOOLEAN:def 3;
(Valid ((p '&' q) => (q '&' p)),J) . v =
(Valid ('not' ((p '&' q) '&' ('not' (q '&' p)))),J) . v
by QC_LANG2:def 2
.=
'not' ((Valid ((p '&' q) '&' ('not' (q '&' p))),J) . v)
by Th20
.=
'not' (((Valid (p '&' q),J) . v) '&' ((Valid ('not' (q '&' p)),J) . v))
by Th22
.=
'not' (((Valid (p '&' q),J) . v) '&' ('not' ((Valid (q '&' p),J) . v)))
by Th20
;
then
((Valid (p '&' q),J) . v) '&' ('not' ((Valid (q '&' p),J) . v)) = TRUE
by A1, MARGREL1:41;
then
(
(Valid (p '&' q),J) . v = TRUE &
'not' ((Valid (q '&' p),J) . v) = TRUE )
by MARGREL1:45;
then
(
(Valid (p '&' q),J) . v = TRUE &
(Valid (q '&' p),J) . v = FALSE )
by MARGREL1:41;
then
(
((Valid p,J) . v) '&' ((Valid q,J) . v) = TRUE &
((Valid q,J) . v) '&' ((Valid p,J) . v) = FALSE )
by Th22;
hence
contradiction
;
:: thesis: verum
end;