theorem thLinPreordEvents: :: PETERSON:2

for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for e1, e2 being Event of DS holds
( e1 <= e2 or e2 <= e1 )