set BS = { (Ext_Borelsubsets_help A) where A is Element of Ext_Borel_Sets : verum } ;
reconsider I = [.0,+infty.] as Subset of ExtREAL by MEMBERED:2;
{ (Ext_Borelsubsets_help A) where A is Element of Ext_Borel_Sets : verum } is non empty Subset-Family of I

proof

reconsider RE = ExtREAL as Element of Ext_Borel_Sets by PROB_1:5;
d1: Ext_Borelsubsets_help RE in { (Ext_Borelsubsets_help A) where A is Element of Ext_Borel_Sets : verum } ;
{ (Ext_Borelsubsets_help A) where A is Element of Ext_Borel_Sets : verum } c= bool I

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (Ext_Borelsubsets_help A) where A is Element of Ext_Borel_Sets : verum } or x in bool I )
assume x in { (Ext_Borelsubsets_help A) where A is Element of Ext_Borel_Sets : verum } ; :: thesis: x in bool I
then consider A being Element of Ext_Borel_Sets such that
D1: x = Ext_Borelsubsets_help A ;
reconsider x = x as set by D1;
x c= I by D1, XBOOLE_0:def 4;
hence x in bool I ; :: thesis: verum

end;

hence { (Ext_Borelsubsets_help A) where A is Element of Ext_Borel_Sets : verum } is non empty Subset-Family of I by d1; :: thesis: verum

end;

then reconsider BS = { (Ext_Borelsubsets_help A) where A is Element of Ext_Borel_Sets : verum } as non empty Subset-Family of I ;
A1: BS is compl-closed

proof

let A be Subset of I; :: according to PROB_1:def 1 :: thesis: ( not A in BS or A ` in BS )
assume A in BS ; :: thesis: A ` in BS
then consider A2 being Element of Ext_Borel_Sets such that
AF1: A = Ext_Borelsubsets_help A2 ;
F2: I \ A = I \ A2 by AF1, XBOOLE_1:47
.= (A2 `) /\ I by SUBSET_1:13 ;
reconsider CA2 = A2 ` as Element of Ext_Borel_Sets by PROB_1:20;
CA2 /\ I = Ext_Borelsubsets_help CA2 ;
hence A ` in BS by F2; :: thesis: verum

end;

BS is sigma-multiplicative

proof

let A1 be SetSequence of I; :: according to PROB_1:def 6 :: thesis: ( not rng A1 c= BS or Intersection A1 in BS )
assume G1: rng A1 c= BS ; :: thesis: Intersection A1 in BS
TT1: for n being Nat holds
( A1 . n in BS & ex A2 being Element of Ext_Borel_Sets st A1 . n = Ext_Borelsubsets_help A2 )

proof

let n be Nat; :: thesis: ( A1 . n in BS & ex A2 being Element of Ext_Borel_Sets st A1 . n = Ext_Borelsubsets_help A2 )
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A1 . n in rng A1 by FUNCT_2:4;
then A1 . n in BS by G1;
hence ( A1 . n in BS & ex A2 being Element of Ext_Borel_Sets st A1 . n = Ext_Borelsubsets_help A2 ) ; :: thesis: verum

end;

rng A1 c= bool ExtREAL

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng A1 or x in bool ExtREAL )
assume d1: x in rng A1 ; :: thesis: x in bool ExtREAL
bool I c= bool ExtREAL by ZFMISC_1:67;
hence x in bool ExtREAL by d1; :: thesis: verum

end;

then reconsider A10 = A1 as SetSequence of ExtREAL by FUNCT_2:6;
for n being Nat holds A10 . n is Event of Ext_Borel_Sets

proof

let n be Nat; :: thesis: A10 . n is Event of Ext_Borel_Sets
ex A2 being Element of Ext_Borel_Sets st A10 . n = Ext_Borelsubsets_help A2 by TT1;
hence A10 . n is Event of Ext_Borel_Sets ; :: thesis: verum

end;

then reconsider A10 = A10 as SetSequence of Ext_Borel_Sets by PROB_1:25;
set UA1 = Union (Complement A10);
for n being Nat holds (Complement A10) . n is Event of Ext_Borel_Sets

proof

let n be Nat; :: thesis: (Complement A10) . n is Event of Ext_Borel_Sets
consider A2 being Element of Ext_Borel_Sets such that
P1: A10 . n = Ext_Borelsubsets_help A2 by TT1;
reconsider A1n = A10 . n as Element of Ext_Borel_Sets by P1;
A1n ` is Element of Ext_Borel_Sets by PROB_1:20;
hence (Complement A10) . n is Event of Ext_Borel_Sets by PROB_1:def 2; :: thesis: verum

end;

then Complement A10 is SetSequence of Ext_Borel_Sets by PROB_1:25;
then reconsider UA1 = Union (Complement A10) as Event of Ext_Borel_Sets by PROB_1:26;
k1: UA1 ` is Event of Ext_Borel_Sets by PROB_1:20;
reconsider IA1 = Intersection A10 as Element of Ext_Borel_Sets by k1;
for x being object holds
( x in IA1 iff x in Ext_Borelsubsets_help IA1 )

proof

let x be object ; :: thesis: ( x in IA1 iff x in Ext_Borelsubsets_help IA1 )
thus ( x in IA1 implies x in Ext_Borelsubsets_help IA1 ) :: thesis: ( x in Ext_Borelsubsets_help IA1 implies x in IA1 )

proof

assume x in IA1 ; :: thesis: x in Ext_Borelsubsets_help IA1
then ( x in IA1 & x in A1 . 0 ) by PROB_1:13;
hence x in Ext_Borelsubsets_help IA1 by XBOOLE_0:def 4; :: thesis: verum

end;

thus ( x in Ext_Borelsubsets_help IA1 implies x in IA1 ) by XBOOLE_0:def 4; :: thesis: verum

end;

then s0: IA1 = Ext_Borelsubsets_help IA1 by TARSKI:2;
Intersection A10 = Intersection A1

proof

for x being object holds
( x in Intersection A10 iff x in Intersection A1 )

proof

let x be object ; :: thesis: ( x in Intersection A10 iff x in Intersection A1 )
( x in Intersection A10 iff for n being Nat holds x in A10 . n ) by PROB_1:13;
then ( x in Intersection A10 iff for n being Nat holds x in A1 . n ) ;
hence ( x in Intersection A10 iff x in Intersection A1 ) by PROB_1:13; :: thesis: verum

end;

hence Intersection A10 = Intersection A1 ; :: thesis: verum

end;

hence Intersection A1 in BS by s0; :: thesis: verum

end;

hence { (Ext_Borelsubsets_help A) where A is Element of Ext_Borel_Sets : verum } is SigmaField of [.0,+infty.] by A1; :: thesis: verum