let A be non empty set ; :: thesis: for J being interpretation of A
for S being Element of CQC-Sub-WFF
for v being Element of Valuations_in A holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S )
let J be interpretation of A; :: thesis: for S being Element of CQC-Sub-WFF
for v being Element of Valuations_in A holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S )
defpred S₁[ Element of CQC-Sub-WFF ] means for v being Element of Valuations_in 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
for x being bound_QC-variable
for SQ being second_Q_comp of [S,x]
for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k
for e being Element of vSUB holds
( S₁[ Sub_P (P,ll,e)] & ( S is Sub_VERUM implies S₁[S] ) & ( S₁[S] implies S₁[ Sub_not S] ) & ( S `2 = S9 `2 & S₁[S] & S₁[S9] implies S₁[ CQCSub_& (S,S9)] ) & ( [S,x] is quantifiable & S₁[S] implies S₁[ CQCSub_All ([S,x],SQ)] ) ) by Th4, Th16, Th20, Th26, Th92;
thus for S being Element of CQC-Sub-WFF holds S₁[S] from SUBLEMMA:sch 1(A1); :: thesis: verum