:: deftheorem defines in PETERSON:def 10 :
for Values being Values_with_Bool
for S being Events_structure over Values
for e being Event of S
for p being Process of S
for tr being trace of S holds
( e in p,tr iff ( e in p & e in tr ) );