let Al be QC-alphabet ; for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (All (x,p)) => p
let A be non empty set ; for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (All (x,p)) => p
let x be bound_QC-variable of Al; for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (All (x,p)) => p
let v be Element of Valuations_in (Al,A); for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (All (x,p)) => p
let p be Element of CQC-WFF Al; for J being interpretation of Al,A holds J,v |= (All (x,p)) => p
let J be interpretation of Al,A; J,v |= (All (x,p)) => p
thus
(Valid (((All (x,p)) => p),J)) . v = TRUE
VALUAT_1:def 7 verumproof
assume
not
(Valid (((All (x,p)) => p),J)) . v = TRUE
;
contradiction
then A1:
(Valid (((All (x,p)) => p),J)) . v = FALSE
by XBOOLEAN:def 3;
(Valid (((All (x,p)) => p),J)) . v =
(Valid (('not' ((All (x,p)) '&' ('not' p))),J)) . v
by QC_LANG2:def 2
.=
'not' ((Valid (((All (x,p)) '&' ('not' p)),J)) . v)
by Th10
.=
'not' (((Valid ((All (x,p)),J)) . v) '&' ((Valid (('not' p),J)) . v))
by Th12
.=
'not' (((Valid ((All (x,p)),J)) . v) '&' ('not' ((Valid (p,J)) . v)))
by Th10
;
then A2:
((Valid ((All (x,p)),J)) . v) '&' ('not' ((Valid (p,J)) . v)) = TRUE
by A1, MARGREL1:11;
then
'not' ((Valid (p,J)) . v) = TRUE
by MARGREL1:12;
then A3:
(Valid (p,J)) . v = FALSE
by MARGREL1:11;
(Valid ((All (x,p)),J)) . v = TRUE
by A2, MARGREL1:12;
then
(FOR_ALL (x,(Valid (p,J)))) . v = TRUE
by Lm1;
hence
contradiction
by A3, Th25;
verum
end;