:: deftheorem Def2 defines |= SUBLEMMA:def 2 :
for Al being QC-alphabet
for S being Element of CQC-Sub-WFF Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for J being interpretation of Al,A holds
( J,v |= S iff J,v |= S `1 );