theorem Th77:
for
Al being
QC-alphabet for
p,
q being
Element of
CQC-WFF Al for
A being non
empty set for
J being
interpretation of
Al,
A st ( for
v being
Element of
Valuations_in (
Al,
A)
for
vS,
vS1,
vS2 being
Val_Sub of
A,
Al st ( for
y being
bound_QC-variable of
Al st
y in dom vS1 holds
not
y in still_not-bound_in p ) & ( for
y being
bound_QC-variable of
Al st
y in dom vS2 holds
vS2 . y = v . y ) &
dom vS misses dom vS2 holds
(
J,
v . vS |= p iff
J,
v . ((vS +* vS1) +* vS2) |= p ) ) & ( for
v being
Element of
Valuations_in (
Al,
A)
for
vS,
vS1,
vS2 being
Val_Sub of
A,
Al st ( for
y being
bound_QC-variable of
Al st
y in dom vS1 holds
not
y in still_not-bound_in q ) & ( for
y being
bound_QC-variable of
Al st
y in dom vS2 holds
vS2 . y = v . y ) &
dom vS misses dom vS2 holds
(
J,
v . vS |= q iff
J,
v . ((vS +* vS1) +* vS2) |= q ) ) holds
for
v being
Element of
Valuations_in (
Al,
A)
for
vS,
vS1,
vS2 being
Val_Sub of
A,
Al st ( for
y being
bound_QC-variable of
Al st
y in dom vS1 holds
not
y in still_not-bound_in (p '&' q) ) & ( for
y being
bound_QC-variable of
Al st
y in dom vS2 holds
vS2 . y = v . y ) &
dom vS misses dom vS2 holds
(
J,
v . vS |= p '&' q iff
J,
v . ((vS +* vS1) +* vS2) |= p '&' q )