let A be QC-alphabet ; for S being Element of QC-Sub-WFF A st S is Sub_universal holds
CQC_Sub S = Quant (S,(CQC_Sub (Sub_the_scope_of S)))
let S be Element of QC-Sub-WFF A; ( S is Sub_universal implies CQC_Sub S = Quant (S,(CQC_Sub (Sub_the_scope_of S))) )
consider F being Function of (QC-Sub-WFF A),(QC-WFF A) such that
A1:
CQC_Sub S = F . S
and
A2:
for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( 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;
consider G being Function of (QC-Sub-WFF A),(QC-WFF A) such that
A3:
CQC_Sub (Sub_the_scope_of S) = G . (Sub_the_scope_of S)
and
A4:
for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies G . S9 = VERUM A ) & ( S9 is Sub_atomic implies G . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies G . S9 = 'not' (G . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies G . S9 = (G . (Sub_the_left_argument_of S9)) '&' (G . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies G . S9 = Quant (S9,(G . (Sub_the_scope_of S9))) ) )
by Def38;
F = G
by A2, A4, Lm6;
hence
( S is Sub_universal implies CQC_Sub S = Quant (S,(CQC_Sub (Sub_the_scope_of S))) )
by A1, A2, A3; verum