theorem :: PETERSON:7

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;