let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A st p is universal holds
ex x being Element of bound_QC-variables A ex q being Element of CQC-WFF A st p = All (x,q)
let p be Element of CQC-WFF A; :: thesis: ( p is universal implies ex x being Element of bound_QC-variables A ex q being Element of CQC-WFF A st p = All (x,q) )
assume p is universal ; :: thesis: ex x being Element of bound_QC-variables A ex q being Element of CQC-WFF A st p = All (x,q)
then consider x being bound_QC-variable of A, q being Element of QC-WFF A such that
A1: p = All (x,q) by QC_LANG1:def 21;
q is Element of CQC-WFF A by A1, CQC_LANG:13;
hence ex x being Element of bound_QC-variables A ex q being Element of CQC-WFF A st p = All (x,q) by A1; :: thesis: verum