:: deftheorem defines val PETERSON:def 9 :
for Values being Values_with_Bool
for S being Events_structure over Values
for e being Event of S holds val e = the val_of of S . e;