theorem Th73: :: SUBLEMMA:73

for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] holds
( ( for a being Element of A holds J,(v . (NEx_Val (v,S,x,xSQ))) . (x | a) |= S ) iff for a being Element of A holds J,(v . (NEx_Val (v,S,x,xSQ))) . (x | a) |= S `1 ) by Def2;