theorem thEvStrictPrec: :: PETERSON:5

for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for p being Process of DS
for e1, e2 being Event of DS st e1 in p & e2 in p & e1 < e2 holds
e1 << e2