theorem Th67:
for
Al being
QC-alphabet for
p being
Element of
CQC-WFF Al for
x being
bound_QC-variable of
Al for
A being non
empty set for
J being
interpretation of
Al,
A st ( for
v,
w being
Element of
Valuations_in (
Al,
A) st
v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
(
J,
v |= p iff
J,
w |= p ) ) holds
for
v,
w being
Element of
Valuations_in (
Al,
A) st
v | (still_not-bound_in (All (x,p))) = w | (still_not-bound_in (All (x,p))) holds
(
J,
v |= All (
x,
p) iff
J,
w |= All (
x,
p) )