:: deftheorem defines reads PETERSON:def 3 :
for Values being Values_with_Bool
for S being Events_structure over Values
for e being Event of S
for x being Location of S holds
( e reads x iff e in the readE of S . x );