:: deftheorem defines inter PETERSON:def 20 :
for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for e1, e2 being Event of DS holds (e1,e2) inter = { e where e is Event of DS : ( e1 < e & e < e2 ) } ;