let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A
for x being Element of bound_QC-variables A holds p is_subformula_of All (x,p)
let p be Element of CQC-WFF A; :: thesis: for x being Element of bound_QC-variables A holds p is_subformula_of All (x,p)
let x be Element of bound_QC-variables A; :: thesis: p is_subformula_of All (x,p)
p is_proper_subformula_of All (x,p) by QC_LANG2:71;
hence p is_subformula_of All (x,p) by QC_LANG2:def 21; :: thesis: verum