:: deftheorem defines interpretation VALUAT_1:def 5 :
for Al being QC-alphabet
for D being non empty set
for b₃ being Function of (QC-pred_symbols Al),(relations_on D) holds
( b₃ is interpretation of Al,D iff for P being Element of QC-pred_symbols Al
for r being Element of relations_on D holds
( not b₃ . P = r or r = empty_rel D or the_arity_of P = the_arity_of r ) );