{ If d 2 Re TypeIjm , (d; di ) 2 ( (Ai))Ijm , for i 2 f1; : : : ; kg, and there is no other individual d0 2 Ijm and attribute A0 su h that (d; d0) 2 ( (A0))Ijm , then V (d) = [[A1: V (d1); : : : ; Ak : V (dk)℄℄.

{ If d 2 SetTypeIjm, (d; di ) 2 memberIjm, for i 2 f1; : : : ; kg, and there is no other individual d0 2 Ijm su h that (d; d0) 2 (member)
Ijm , then V (d) =
fV (d1 ); : : : ; V (dk)g.
 For every lass name C, S (I)
(C) = fV (d) j d 2 ( (C))Ijm g.

 S (I) = f(o; v) j V (d1) = o; V (d2) = v; and (d1; d2) 2 valueIjm g.

We rst prove that for ea h on ept (T ), whi
h is the translation of a type expression T of S, and ea h d 2 Ijm, d 2 ( (T ))Ijm if and only if V (d) 2 T S (I). The proof is by indu tion on the stru ture of the on ept expression. Again for the indu tive part we restri t our attention to the ase of re ord types.

Base ase: T = C (i.e., (T ) is an atomi 
on
ept). If d 2 ( (C))Ijm then V (d) 2 CS (I)
, and vi e-versa if o 2 CS (I)
then 1 V (o) 2 ( (C))Ijm .

Indu tive ase: (T ) = Re
Type u 8 (A1). (T1 ) u 9=1 (A1) u    u 8 (Ak). (Tk) u 9=1 (Ak ) and T = Re
ord A1: T1; : : : ; Ak: Tk End. We assume that d 2 ( (Ti ))Ijm i V (d) 2 T
S (I)
i
, for i 2 f1; : : : ; kg, and show that d 2 ( (T ))Ijm i V (d) 2 T S (I).

Suppose that d 2 ( (T ))Ijm . Then d 2 Re
TypeIjm and for ea
h i 2 f1; : : : ; kg there is an individual di su
h that di 2 ( (Ti))Ijm and (d; di ) 2 ( (Ai))Ijm . By 
onstru
tion V (d) = [[A1: v1; : : : ; Ah: vh℄℄ for some h  k. Moreover, by indu
tion hypothesis V (di) 2 T

S (I)
i and therefore V (d) 2 T S (I).

Conversely, suppose that V (d) 2 T S (I), i.e., V (d) = [[A1: v1; : : : ; Ah: vh℄℄ with h  k and vi 2 T
S (I)
i for i 2 f1; : : : ; kg. By indu
tion hypothesis di = 1 V (vi) 2 ( (Ti))Ijm ,
for i 2 f1; : : : ; kg, and by denition of V , d 2 Re
TypeIjm and (d; di ) 2 ( (Ai))Ijm ,
for i 2 f1; : : : ; kg. Sin
e all roles (A) 
orresponding to attribute names are fun
tional, d 2 ( (T ))Ijm .

It remains to show that for ea h de laration

$${\bf\nabla}\cdot{\bf\nabla}\;\;\;{\bf\nabla}-{\bf\nabla}\eta$$

Class C is-a C1; : : : ; Cn type-is T
in DS , (a) CS (I)  CS (I)
i for ea
h i 2 f1; : : : ; ng, and (b) S (I)(CS (I))  T S (I).

(a) follows from the fa t that (S) 
ontains the assertion (C) _ (C1) u    u (Cn)
and from the denition of S (I)
.

(b) follows from what we have shown above and from the fa t that Ijm still satises the assertion (C) _ Abstra
tClass u 8value. (T ). In fa
t, for some d 2 ( (C))Ilet d0be the unique individual su h that (d; d0) 2 valueI. Sin
e I is a model of (S), d02 ( (T ))I.

We argue that also d0 2 ( (T ))Ijm . If d0is not part of a bad 
y
le in I, then I and Ijm 
oin
ide on the sub-stru
ture rooted at d0and formed by the individuals rea
hed via member and roles orresponding to attributes, and we are done. Otherwise, in Ijm su
h sub-stru ture is expanded into a nite tree. Sin e by onstru tion the depth of this tree is at least depth (T ), and the onne tions between individuals in I are preserved in Ijm, it follows that d0 2 ( (T ))Ijm .