let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable holds All (x,p) |-| p
let x be bound_QC-variable; :: 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 by Def1; :: 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) by Def1; :: thesis: verum