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 19;
q is Element of CQC-WFF by A1, CQC_LANG:13;
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