let Al be QC-alphabet ; for A being non empty set
for J being interpretation of Al,A
for S being Element of CQC-Sub-WFF Al
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S )
let A be non empty set ; for J being interpretation of Al,A
for S being Element of CQC-Sub-WFF Al
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S )
let J be interpretation of Al,A; for S being Element of CQC-Sub-WFF Al
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S )
defpred S1[ Element of CQC-Sub-WFF Al] means for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub $1 iff J,v . (Val_S (v,$1)) |= $1 );
A1:
for S, S9 being Element of CQC-Sub-WFF Al
for x being bound_QC-variable of Al
for SQ being second_Q_comp of [S,x]
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al
for e being Element of vSUB Al holds
( S1[ Sub_P (P,ll,e)] & ( S is Al -Sub_VERUM implies S1[S] ) & ( S1[S] implies S1[ Sub_not S] ) & ( S `2 = S9 `2 & S1[S] & S1[S9] implies S1[ CQCSub_& (S,S9)] ) & ( [S,x] is quantifiable & S1[S] implies S1[ CQCSub_All ([S,x],SQ)] ) )
by Th4, Th15, Th19, Th25, Th88;
thus
for S being Element of CQC-Sub-WFF Al holds S1[S]
from SUBLEMMA:sch 1(A1); verum