theorem :: PETERSON:6

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 st e1 in p,tr & e2 in p,tr & e1 < e2 holds
e1 << e2 by thEvStrictPrec;