let Al be QC-alphabet ; :: thesis: 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 )
let p, q be Element of CQC-WFF Al; :: thesis: 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 )
let A be non empty set ; :: thesis: 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 )
let J be interpretation of Al,A; :: thesis: ( ( 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 ) ) implies 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 ) )
assume A1: ( ( 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 ) ) ) ; :: thesis: 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 )
set X = (still_not-bound_in p) \/ (still_not-bound_in q);
let v, w be Element of Valuations_in (Al,A); :: thesis: ( v | (still_not-bound_in (p '&' q)) = w | (still_not-bound_in (p '&' q)) implies ( J,v |= p '&' q iff J,w |= p '&' q ) )
A2: still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q) by QC_LANG3:10;
assume v | (still_not-bound_in (p '&' q)) = w | (still_not-bound_in (p '&' q)) ; :: thesis: ( J,v |= p '&' q iff J,w |= p '&' q )
then ( v | (still_not-bound_in p) = w | (still_not-bound_in p) & v | (still_not-bound_in q) = w | (still_not-bound_in q) ) by A2, RELAT_1:153, XBOOLE_1:7;
then ( J,v |= p & J,v |= q iff ( J,w |= p & J,w |= q ) ) by A1;
hence ( J,v |= p '&' q iff J,w |= p '&' q ) by VALUAT_1:18; :: thesis: verum