theorem :: VALUAT_1:39

for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A holds J |= VERUM Al by Th32;