theorem Th56:
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
v being
Element of
Valuations_in (
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
a being
Element of
A holds
J,
(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ)) +* (x | a)) |= S ) iff for
a being
Element of
A holds
J,
(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a)) |= S )