let Al be QC-alphabet ; :: thesis: for p 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 ) ) holds
for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in ('not' p)) = w | (still_not-bound_in ('not' p)) holds
( J,v |= 'not' p iff J,w |= 'not' p )
let p 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 ) ) holds
for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in ('not' p)) = w | (still_not-bound_in ('not' p)) holds
( J,v |= 'not' p iff J,w |= 'not' p )
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 ) ) holds
for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in ('not' p)) = w | (still_not-bound_in ('not' p)) holds
( J,v |= 'not' p iff J,w |= 'not' p )
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 ) ) implies for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in ('not' p)) = w | (still_not-bound_in ('not' p)) holds
( J,v |= 'not' p iff J,w |= 'not' p ) )
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 ) ; :: thesis: for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in ('not' p)) = w | (still_not-bound_in ('not' p)) holds
( J,v |= 'not' p iff J,w |= 'not' p )
let v, w be Element of Valuations_in (Al,A); :: thesis: ( v | (still_not-bound_in ('not' p)) = w | (still_not-bound_in ('not' p)) implies ( J,v |= 'not' p iff J,w |= 'not' p ) )
A2: still_not-bound_in ('not' p) = still_not-bound_in p by QC_LANG3:7;
assume v | (still_not-bound_in ('not' p)) = w | (still_not-bound_in ('not' p)) ; :: thesis: ( J,v |= 'not' p iff J,w |= 'not' p )
then ( not J,v |= p iff not J,w |= p ) by A1, A2;
hence ( J,v |= 'not' p iff J,w |= 'not' p ) by VALUAT_1:17; :: thesis: verum