let Al be QC-alphabet ; :: thesis: for A being non empty set
for J being interpretation of Al,A
for p being Element of CQC-WFF Al
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 )
let A be non empty set ; :: thesis: for J being interpretation of Al,A
for p being Element of CQC-WFF Al
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 )
let J be interpretation of Al,A; :: thesis: for p being Element of CQC-WFF Al
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 )
defpred S₁[ Element of CQC-WFF Al] means 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 $1 ) & ( 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 |= $1 iff J,v . ((vS +* vS1) +* vS2) |= $1 );
A1: for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( S₁[ VERUM Al] & S₁[P ! l] & ( S₁[p] implies S₁[ 'not' p] ) & ( S₁[p] & S₁[q] implies S₁[p '&' q] ) & ( S₁[p] implies S₁[ All (x,p)] ) ) by Th75, Th76, Th77, Th80, VALUAT_1:32;
thus for p being Element of CQC-WFF Al holds S₁[p] from CQC_LANG:sch 1(A1); :: thesis: verum