theorem Th6: :: SUBLEMMA:6

for Al being QC-alphabet
for S being Element of CQC-Sub-WFF Al st S is Sub_atomic holds
CQC_Sub S = (the_pred_symbol_of (S `1)) ! (CQC_Subst ((Sub_the_arguments_of S),(S `2)))