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, S' 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
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 = S' `2 & S₁[S] & S₁[S'] implies S₁[ CQCSub_& S,S'] ) & ( [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