let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds All (x,p) |-| p
let p be Element of CQC-WFF A; :: thesis: for x being bound_QC-variable of A holds All (x,p) |-| p
let x be bound_QC-variable of A; :: thesis: All (x,p) |-| p
{(All (x,p))} |- (All (x,p)) => p by CQC_THE1:56;
then {(All (x,p))} |- p by CQC_THE1:55, CQC_THE2:87;
hence All (x,p) |- p ; :: according to CQC_THE3:def 5 :: thesis: p |- All (x,p)
{p} |- p by CQC_THE2:87;
then {p} |- All (x,p) by Th35;
hence p |- All (x,p) ; :: thesis: verum