theorem :: PROB_1:20

for X being set
for Si being SigmaField of X
for A being Event of Si holds A ` is Event of Si by Def1;