theorem Th30: :: SUBSTUT1:30

for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_conjunctive holds
CQC_Sub S = (CQC_Sub (Sub_the_left_argument_of S)) '&' (CQC_Sub (Sub_the_right_argument_of S))