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