let Al be QC-alphabet ; for A being non empty set
for J being interpretation of Al,A
for p being Element of CQC-WFF Al
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 )
let A be non empty set ; for J being interpretation of Al,A
for p being Element of CQC-WFF Al
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 )
let J be interpretation of Al,A; for p being Element of CQC-WFF Al
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 )
defpred S1[ Element of CQC-WFF Al] means for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in $1) = w | (still_not-bound_in $1) holds
( J,v |= $1 iff J,w |= $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
( S1[ VERUM Al] & S1[P ! l] & ( S1[p] implies S1[ 'not' p] ) & ( S1[p] & S1[q] implies S1[p '&' q] ) & ( S1[p] implies S1[ All (x,p)] ) )
by Th60, Th61, Th62, Th67, VALUAT_1:32;
thus
for p being Element of CQC-WFF Al holds S1[p]
from CQC_LANG:sch 1(A1); verum