theorem :: PETERSON:13

for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for e1, e2 being Event of DS holds
( simultev e1,e2 or e1 << e2 or e2 << e1 ) by thLinPreordEvents;