let p be Element of CQC-WFF ; :: thesis: for x being Element of bound_QC-variables holds p is_subformula_of All x,p
let x be Element of bound_QC-variables ; :: thesis: p is_subformula_of All x,p
p is_proper_subformula_of All x,p by QC_LANG2:91;
hence p is_subformula_of All x,p by QC_LANG2:def 22; :: thesis: verum