theorem :: PETERSON:8

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 & not e1 = e2 & not e1 << e2 holds
e2 << e1 by thLinPreordEvents, thEvStrictPrec, ORDERS_2:def 6;