for X, x being set
for Si being SigmaField of X st x in Si holds
x is Event of Si ;