theorem Th5: :: SUBSTUT2:5

for Al being QC-alphabet
for p, q being Element of CQC-WFF Al st ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st
( S `1 = p & S `2 = Sub ) ) & ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st
( S `1 = q & S `2 = Sub ) ) holds
for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st
( S `1 = p '&' q & S `2 = Sub )