let B be CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :]; :: thesis: for SQ being second_Q_comp of B st B is quantifiable holds
CQCSub_All B,SQ is Sub_universal
let SQ be second_Q_comp of B; :: thesis: ( B is quantifiable implies CQCSub_All B,SQ is Sub_universal )
assume A1: B is quantifiable ; :: thesis: CQCSub_All B,SQ is Sub_universal
then Sub_All B,SQ is Sub_universal by SUBSTUT1:14;
hence CQCSub_All B,SQ is Sub_universal by A1, Def6; :: thesis: verum