theorem :: VALUAT_1:4

for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A holds Valid ((VERUM Al),J) = (Valuations_in (Al,A)) --> TRUE by Lm1;