let A be non empty set ; :: thesis: for J being interpretation of A
for p being Element of CQC-WFF
for v, w being Element of Valuations_in 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 A; :: thesis: for p being Element of CQC-WFF
for v, w being Element of Valuations_in A st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
( J,v |= p iff J,w |= p )
defpred S₁[ Element of CQC-WFF ] means for v, w being Element of Valuations_in 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
for x being bound_QC-variable
for k being Element of NAT
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( S₁[ VERUM ] & 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 Th61, Th62, Th63, Th68, VALUAT_1:32;
thus for p being Element of CQC-WFF holds S₁[p] from CQC_LANG:sch 1(A1); :: thesis: verum