set C = Sigma;
A1: {Sigma} c= bool Sigma by ZFMISC_1:68;
Sigma is Element of bool Sigma
proof
Sigma in {Sigma} by TARSKI:def 1;
hence Sigma is Element of bool Sigma by A1; :: thesis: verum
end;
then reconsider C = Sigma as Element of bool Sigma ;
set const = I --> C;
reconsider const = I --> C as Function of I,(bool Sigma) ;
Z1: for i being set st i in I holds
const . i is SigmaField of Omega by FUNCOP_1:7;
T1: const is ManySortedSigmaField of I,Sigma by Z1, KOLMOG01:def 2;
for x, y being Element of I st x <= y holds
const . x is Subset of (const . y)
proof
let x, y be Element of I; :: thesis: ( x <= y implies const . x is Subset of (const . y) )
assume x <= y ; :: thesis: const . x is Subset of (const . y)
( const . x = C & const . y = C ) by FUNCOP_1:7;
hence const . x is Subset of (const . y) ; :: thesis: verum
end;
hence ex b1 being ManySortedSigmaField of I,Sigma st
for s, t being Element of I st s <= t holds
b1 . s is Subset of (b1 . t) by T1; :: thesis: verum