for Al being 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 )