let S be Element of QC-Sub-WFF ; :: thesis: ( S is Sub_VERUM implies CQC_Sub S is Element of CQC-WFF )
assume A1: S is Sub_VERUM ; :: thesis: CQC_Sub S is Element of CQC-WFF
ex F being Function of QC-Sub-WFF ,QC-WFF st
( CQC_Sub S = F . S & ( for S9 being Element of QC-Sub-WFF holds
( ( S9 is Sub_VERUM implies F . S9 = VERUM ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1 )) ! (CQC_Subst (Sub_the_arguments_of S9),(S9 `2 )) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant S9,(F . (Sub_the_scope_of S9)) ) ) ) ) by Def38;
hence CQC_Sub S is Element of CQC-WFF by A1; :: thesis: verum