:: deftheorem defines reads PETERSON:def 5 :
for Values being Values_with_Bool
for S being Events_structure over Values
for x being Location of S
for E being EventSet of S holds
( E reads x iff ex e being Event of S st
( e in E & e reads x ) );