let p be Element of CQC-WFF ; :: thesis: for A being non empty set
for J being interpretation of A st ( for v being Element of Valuations_in A
for vS, vS1, vS2 being Val_Sub of A st ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in p ) & ( for y being bound_QC-variable 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 ) ) holds
for v being Element of Valuations_in A
for vS, vS1, vS2 being Val_Sub of A st ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in ('not' p) ) & ( for y being bound_QC-variable st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= 'not' p iff J,v . ((vS +* vS1) +* vS2) |= 'not' p )
let A be non empty set ; :: thesis: for J being interpretation of A st ( for v being Element of Valuations_in A
for vS, vS1, vS2 being Val_Sub of A st ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in p ) & ( for y being bound_QC-variable 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 ) ) holds
for v being Element of Valuations_in A
for vS, vS1, vS2 being Val_Sub of A st ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in ('not' p) ) & ( for y being bound_QC-variable st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= 'not' p iff J,v . ((vS +* vS1) +* vS2) |= 'not' p )
let J be interpretation of A; :: thesis: ( ( for v being Element of Valuations_in A
for vS, vS1, vS2 being Val_Sub of A st ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in p ) & ( for y being bound_QC-variable 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 ) ) implies for v being Element of Valuations_in A
for vS, vS1, vS2 being Val_Sub of A st ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in ('not' p) ) & ( for y being bound_QC-variable st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= 'not' p iff J,v . ((vS +* vS1) +* vS2) |= 'not' p ) )
assume A1: for v being Element of Valuations_in A
for vS, vS1, vS2 being Val_Sub of A st ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in p ) & ( for y being bound_QC-variable 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 ) ; :: thesis: for v being Element of Valuations_in A
for vS, vS1, vS2 being Val_Sub of A st ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in ('not' p) ) & ( for y being bound_QC-variable st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= 'not' p iff J,v . ((vS +* vS1) +* vS2) |= 'not' p )
let v be Element of Valuations_in A; :: thesis: for vS, vS1, vS2 being Val_Sub of A st ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in ('not' p) ) & ( for y being bound_QC-variable st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= 'not' p iff J,v . ((vS +* vS1) +* vS2) |= 'not' p )
let vS, vS1, vS2 be Val_Sub of A; :: thesis: ( ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in ('not' p) ) & ( for y being bound_QC-variable st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 implies ( J,v . vS |= 'not' p iff J,v . ((vS +* vS1) +* vS2) |= 'not' p ) )
assume A2: ( ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in ('not' p) ) & ( for y being bound_QC-variable st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 ) ; :: thesis: ( J,v . vS |= 'not' p iff J,v . ((vS +* vS1) +* vS2) |= 'not' p )
for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in p

proof

let y be bound_QC-variable; :: thesis: ( y in dom vS1 implies not y in still_not-bound_in p )
assume y in dom vS1 ; :: thesis: not y in still_not-bound_in p
then not y in still_not-bound_in ('not' p) by A2;
hence not y in still_not-bound_in p by QC_LANG3:11; :: thesis: verum

end;

then ( not J,v . vS |= p iff not J,v . ((vS +* vS1) +* vS2) |= p ) by A1, A2;
hence ( J,v . vS |= 'not' p iff J,v . ((vS +* vS1) +* vS2) |= 'not' p ) by VALUAT_1:28; :: thesis: verum