theorem Th62:
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,
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 ) ) & ( for
v,
w being
Element of
Valuations_in (
Al,
A) st
v | (still_not-bound_in q) = w | (still_not-bound_in q) holds
(
J,
v |= q iff
J,
w |= q ) ) holds
for
v,
w being
Element of
Valuations_in (
Al,
A) st
v | (still_not-bound_in (p '&' q)) = w | (still_not-bound_in (p '&' q)) holds
(
J,
v |= p '&' q iff
J,
w |= p '&' q )