:: deftheorem defines pr-ordered PETERSON:def 14 :
for Values being Values_with_Bool
for S being Events_structure over Values holds
( S is pr-ordered iff for p being Process of S
for e1, e2 being Event of S st e1 in p & e2 in p & e1 <= e2 & e2 <= e1 holds
e1 = e2 );