let Omega be non empty set ; :: thesis:
let Sigma be SigmaField of Omega; :: thesis:
let T be Nat; :: thesis:
let TFix be Element of StoppingSetExt T; :: thesis:
let MyFunc be Filtration of StoppingSet T,Sigma; :: thesis:
set const = Omega --> TFix;
for t being Element of StoppingSet T holds { w where w is Element of Omega : (Omega --> TFix) . w = t } in MyFunc . t

C1: { w where w is Element of Omega : (Omega --> TFix) . w = t } = Omega

for x being object holds
( x in { w where w is Element of Omega : (Omega --> TFix) . w = t } iff x in Omega )

let x be object ; :: thesis:
thus ( x in { w where w is Element of Omega : (Omega --> TFix) . w = t } implies x in Omega ) :: thesis:

assume x in { w where w is Element of Omega : (Omega --> TFix) . w = t } ; :: thesis:
then consider s being Element of Omega such that
E1: ( s = x & (Omega --> TFix) . s = t ) ;
thus x in Omega by E1; :: thesis:

end;

assume x in Omega ; :: thesis:
then consider y being Element of Omega such that
F10: ( y = x & y in Omega ) ;
( y in Omega implies t = (Omega --> TFix) . y ) by FUNCOP_1:7, S0;
hence x in { w where w is Element of Omega : (Omega --> TFix) . w = t } by F10; :: thesis:

end;

hence { w where w is Element of Omega : (Omega --> TFix) . w = t } = Omega by TARSKI:2; :: thesis:

end;

end;

c1: { w where w is Element of Omega : (Omega --> TFix) . w = t } c= {}

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { w where w is Element of Omega : (Omega --> TFix) . w = t } ; :: thesis:
then ex s being Element of Omega st
( s = x & (Omega --> TFix) . s = t ) ;
then consider s being Element of Omega such that
E1: ( s = x & (Omega --> TFix) . s <> TFix ) by S1;
thus x in {} by E1, FUNCOP_1:7; :: thesis:

end;

MyFunc . t is SigmaField of Omega by KOLMOG01:def 2;
then {} in MyFunc . t by PROB_1:4;
hence { w where w is Element of Omega : (Omega --> TFix) . w = t } in MyFunc . t by c1; :: thesis:

end;