theorem :: PETERSON:4

for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for e1, e2 being Event of DS st e1 < e2 holds
e1 <= e2 by ORDERS_2:def 6;