theorem Th87: :: SUBLEMMA:87

for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
for v being Element of Valuations_in (Al,A) holds
( J,v . (NEx_Val (v,S,x,xSQ)) |= All (x,(S `1)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) )