 The idea behind this definition is to express in the correspondence language the semantic interpretation of the modal formulas: both languages are talking about the same structures, as a Kripke structure can be viewed as a plain first-order relational structure. From this definition the following equivalence is obtained: