for X being set
for Si being SigmaField of X holds X is Event of Si by Th5;