for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for p being Process of DS
for tr being trace of DS
for e1, e2 being Event of DS holds (e1,e2) interval_in (p,tr) c= (e1,e2) inter