defpred S₁[ set ] means (A ^\ s) . Omega is Event of Sigma;
thus A ^\ s is Sigma -valued ; :: thesis: verum