theorem Th15: :: SUBLEMMA:15

for Al being QC-alphabet
for k being Nat
for A being non empty set
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub (Sub_P (P,ll,Sub)) iff J,v . (Val_S (v,(Sub_P (P,ll,Sub)))) |= Sub_P (P,ll,Sub) )