theorem :: PETERSON:3

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 e, e1, e2 being Event of DS st e in p,tr & e1 < e & e < e2 holds
e in (e1,e2) interval_in (p,tr) ;