theorem thEvStrictTrans2: :: PETERSON:11

for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for e1, e2, e3 being Event of DS st e1 << e2 & e2 <= e3 holds
e1 << e3 by thEvTrans;