for Al being QC-alphabet
for PHI being Consistent Subset of (CQC-WFF Al)
for Al2 being b₁ -expanding QC-alphabet
for THETA being Subset of (CQC-WFF Al2) st PHI = THETA holds
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st J,v |= PHI holds
ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA