set BS = { (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } ;

{ (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } is non empty Subset-Family of I

A1: BS is compl-closed

{ (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } is non empty Subset-Family of I

proof

then reconsider BS = { (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } as non empty Subset-Family of I ;
reconsider RE = REAL as Element of Borel_Sets by PROB_1:5;

d1: Borelsubsets_help (RE,I) in { (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } ;

{ (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } c= bool I

end;d1: Borelsubsets_help (RE,I) in { (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } ;

{ (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } c= bool I

proof

hence
{ (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } is non empty Subset-Family of I
by d1; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } or x in bool I )

assume x in { (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } ; :: thesis: x in bool I

then consider A being Element of Borel_Sets such that

D1: x = Borelsubsets_help (A,I) ;

reconsider x = x as set by D1;

x c= I by D1, XBOOLE_0:def 4;

hence x in bool I ; :: thesis: verum

end;assume x in { (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } ; :: thesis: x in bool I

then consider A being Element of Borel_Sets such that

D1: x = Borelsubsets_help (A,I) ;

reconsider x = x as set by D1;

x c= I by D1, XBOOLE_0:def 4;

hence x in bool I ; :: thesis: verum

A1: BS is compl-closed

proof

BS is sigma-multiplicative
for A being Subset of I st A in BS holds

A ` in BS

end;A ` in BS

proof

hence
BS is compl-closed
; :: thesis: verum
let A be Subset of I; :: thesis: ( A in BS implies A ` in BS )

assume A in BS ; :: thesis: A ` in BS

then consider A2 being Element of Borel_Sets such that

AF1: A = Borelsubsets_help (A2,I) ;

F2: I \ A = (A2 `) /\ I

CA2 /\ I = Borelsubsets_help (CA2,I) ;

hence A ` in BS by F2; :: thesis: verum

end;assume A in BS ; :: thesis: A ` in BS

then consider A2 being Element of Borel_Sets such that

AF1: A = Borelsubsets_help (A2,I) ;

F2: I \ A = (A2 `) /\ I

proof

reconsider CA2 = A2 ` as Element of Borel_Sets by PROB_1:20;
for x being object holds

( x in I \ A iff x in (A2 `) /\ I )

end;( x in I \ A iff x in (A2 `) /\ I )

proof

hence
I \ A = (A2 `) /\ I
; :: thesis: verum
let x be object ; :: thesis: ( x in I \ A iff x in (A2 `) /\ I )

thus ( x in I \ A implies x in (A2 `) /\ I ) :: thesis: ( x in (A2 `) /\ I implies x in I \ A )

then ( x in A2 ` & x in I ) by XBOOLE_0:def 4;

then ( x in I & x in REAL & not x in A2 ) by XBOOLE_0:def 5;

then ( x in I & not x in A2 /\ I ) by XBOOLE_0:def 4;

hence x in I \ A by XBOOLE_0:def 5, AF1; :: thesis: verum

end;thus ( x in I \ A implies x in (A2 `) /\ I ) :: thesis: ( x in (A2 `) /\ I implies x in I \ A )

proof

assume
x in (A2 `) /\ I
; :: thesis: x in I \ A
assume ASS0:
x in I \ A
; :: thesis: x in (A2 `) /\ I

reconsider I = I as Subset of REAL ;

( x in I & not x in A ) by ASS0, XBOOLE_0:def 5;

then ( x in I & ( not x in A2 or not x in I ) ) by XBOOLE_0:def 4, AF1;

then ( x in I & x in REAL \ A2 ) by XBOOLE_0:def 5;

hence x in (A2 `) /\ I by XBOOLE_0:def 4; :: thesis: verum

end;reconsider I = I as Subset of REAL ;

( x in I & not x in A ) by ASS0, XBOOLE_0:def 5;

then ( x in I & ( not x in A2 or not x in I ) ) by XBOOLE_0:def 4, AF1;

then ( x in I & x in REAL \ A2 ) by XBOOLE_0:def 5;

hence x in (A2 `) /\ I by XBOOLE_0:def 4; :: thesis: verum

then ( x in A2 ` & x in I ) by XBOOLE_0:def 4;

then ( x in I & x in REAL & not x in A2 ) by XBOOLE_0:def 5;

then ( x in I & not x in A2 /\ I ) by XBOOLE_0:def 4;

hence x in I \ A by XBOOLE_0:def 5, AF1; :: thesis: verum

CA2 /\ I = Borelsubsets_help (CA2,I) ;

hence A ` in BS by F2; :: thesis: verum

proof

hence
{ (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } is SigmaField of I
by A1; :: thesis: verum
for A1 being SetSequence of I st rng A1 c= BS holds

Intersection A1 in BS

end;Intersection A1 in BS

proof

hence
BS is sigma-multiplicative
; :: thesis: verum
let A1 be SetSequence of I; :: thesis: ( rng A1 c= BS implies 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 Borel_Sets st A1 . n = Borelsubsets_help (A2,I) )

for n being Nat holds A10 . n is Event of Borel_Sets

set UA1 = Union (Complement A10);

for n being Nat holds (Complement A10) . n is Event of Borel_Sets

then reconsider UA1 = Union (Complement A10) as Event of Borel_Sets by PROB_1:26;

k1: UA1 ` is Event of Borel_Sets by PROB_1:20;

reconsider IA1 = Intersection A10 as Element of Borel_Sets by k1;

s0: ( IA1 in BS & IA1 = Borelsubsets_help (IA1,I) )

end;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 Borel_Sets st A1 . n = Borelsubsets_help (A2,I) )

proof

rng A1 c= bool REAL
let n be Nat; :: thesis: ( A1 . n in BS & ex A2 being Element of Borel_Sets st A1 . n = Borelsubsets_help (A2,I) )

A1 . n in rng A1 by FUNCT_2:4, ORDINAL1:def 12;

then A1 . n in BS by G1;

hence ( A1 . n in BS & ex A2 being Element of Borel_Sets st A1 . n = Borelsubsets_help (A2,I) ) ; :: thesis: verum

end;A1 . n in rng A1 by FUNCT_2:4, ORDINAL1:def 12;

then A1 . n in BS by G1;

hence ( A1 . n in BS & ex A2 being Element of Borel_Sets st A1 . n = Borelsubsets_help (A2,I) ) ; :: thesis: verum

proof

then reconsider A10 = A1 as SetSequence of REAL by FUNCT_2:6;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng A1 or x in bool REAL )

assume d1: x in rng A1 ; :: thesis: x in bool REAL

bool I c= bool REAL by ZFMISC_1:67;

hence x in bool REAL by d1; :: thesis: verum

end;assume d1: x in rng A1 ; :: thesis: x in bool REAL

bool I c= bool REAL by ZFMISC_1:67;

hence x in bool REAL by d1; :: thesis: verum

for n being Nat holds A10 . n is Event of Borel_Sets

proof

then reconsider A10 = A10 as SetSequence of Borel_Sets by PROB_1:25;
let n be Nat; :: thesis: A10 . n is Event of Borel_Sets

ex A2 being Element of Borel_Sets st A10 . n = Borelsubsets_help (A2,I) by TT1;

hence A10 . n is Event of Borel_Sets ; :: thesis: verum

end;ex A2 being Element of Borel_Sets st A10 . n = Borelsubsets_help (A2,I) by TT1;

hence A10 . n is Event of Borel_Sets ; :: thesis: verum

set UA1 = Union (Complement A10);

for n being Nat holds (Complement A10) . n is Event of Borel_Sets

proof

then
Complement A10 is SetSequence of Borel_Sets
by PROB_1:25;
let n be Nat; :: thesis: (Complement A10) . n is Event of Borel_Sets

consider A2 being Element of Borel_Sets such that

P1: A10 . n = Borelsubsets_help (A2,I) by TT1;

reconsider A1n = A10 . n as Element of Borel_Sets by P1;

A1n ` is Element of Borel_Sets by PROB_1:20;

hence (Complement A10) . n is Event of Borel_Sets by PROB_1:def 2; :: thesis: verum

end;consider A2 being Element of Borel_Sets such that

P1: A10 . n = Borelsubsets_help (A2,I) by TT1;

reconsider A1n = A10 . n as Element of Borel_Sets by P1;

A1n ` is Element of Borel_Sets by PROB_1:20;

hence (Complement A10) . n is Event of Borel_Sets by PROB_1:def 2; :: thesis: verum

then reconsider UA1 = Union (Complement A10) as Event of Borel_Sets by PROB_1:26;

k1: UA1 ` is Event of Borel_Sets by PROB_1:20;

reconsider IA1 = Intersection A10 as Element of Borel_Sets by k1;

s0: ( IA1 in BS & IA1 = Borelsubsets_help (IA1,I) )

proof

Intersection A10 = Intersection A1
for x being object holds

( x in IA1 iff x in Borelsubsets_help (IA1,I) )

hence ( IA1 in BS & IA1 = Borelsubsets_help (IA1,I) ) ; :: thesis: verum

end;( x in IA1 iff x in Borelsubsets_help (IA1,I) )

proof

then
IA1 = Borelsubsets_help (IA1,I)
by TARSKI:2;
let x be object ; :: thesis: ( x in IA1 iff x in Borelsubsets_help (IA1,I) )

thus ( x in IA1 implies x in Borelsubsets_help (IA1,I) ) :: thesis: ( x in Borelsubsets_help (IA1,I) implies x in IA1 )

end;thus ( x in IA1 implies x in Borelsubsets_help (IA1,I) ) :: thesis: ( x in Borelsubsets_help (IA1,I) implies x in IA1 )

proof

thus
( x in Borelsubsets_help (IA1,I) implies x in IA1 )
by XBOOLE_0:def 4; :: thesis: verum
assume
x in IA1
; :: thesis: x in Borelsubsets_help (IA1,I)

then ( x in IA1 & x in A1 . 0 ) by PROB_1:13;

hence x in Borelsubsets_help (IA1,I) by XBOOLE_0:def 4; :: thesis: verum

end;then ( x in IA1 & x in A1 . 0 ) by PROB_1:13;

hence x in Borelsubsets_help (IA1,I) by XBOOLE_0:def 4; :: thesis: verum

hence ( IA1 in BS & IA1 = Borelsubsets_help (IA1,I) ) ; :: thesis: verum

proof

hence
Intersection A1 in BS
by s0; :: thesis: verum
for x being object holds

( x in Intersection A10 iff x in Intersection A1 )

end;( x in Intersection A10 iff x in Intersection A1 )

proof

hence
Intersection A10 = Intersection A1
; :: thesis: verum
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;( 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