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:93;
then {(All x,p)} |- p by CQC_THE1:92, CQC_THE2:91;
hence All x,p |- p by Def1; :: according to CQC_THE3:def 5 :: thesis: p |- All x,p
{p} |- p by CQC_THE2:91;
then {p} |- All x,p by Th35;
hence p |- All x,p by Def1; :: thesis: verum