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

proof

assume not (Valid ((All x,p) => p),J) . v = TRUE ; :: thesis: 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 Th20
.= 'not' (((Valid (All x,p),J) . v) '&' ((Valid ('not' p),J) . v)) by Th22
.= 'not' (((Valid (All x,p),J) . v) '&' ('not' ((Valid p,J) . v))) by Th20 ;
then A2: ((Valid (All x,p),J) . v) '&' ('not' ((Valid p,J) . v)) = TRUE by A1, MARGREL1:41;
then 'not' ((Valid p,J) . v) = TRUE by MARGREL1:45;
then A3: (Valid p,J) . v = FALSE by MARGREL1:41;
(Valid (All x,p),J) . v = TRUE by A2, MARGREL1:45;
then (FOR_ALL x,(Valid p,J)) . v = TRUE by Lm1;
hence contradiction by A3, Th37; :: thesis: verum

end;