theorem Th35: :: SUBLEMMA:35

for Al being QC-alphabet
for B being CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
for SQ being second_Q_comp of B
for B1 being Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
for SQ1 being second_Q_comp of B1 st B is quantifiable & B1 is quantifiable & Sub_All (B,SQ) = Sub_All (B1,SQ1) holds
( B `2 = B1 `2 & SQ = SQ1 )