theorem :: CQC_SIM1:40

for A being QC-alphabet
for t being QC-symbol of A
for p, q being Element of CQC-WFF A
for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
for K being Element of Fin (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p holds
not x. t in f .: K