consider A1 being SetSequence of REAL such that
A1: for n being Nat holds A1 . n = {n} by Q00;
consider A2 being SetSequence of REAL such that
A2: for n being Nat holds A2 . n = {(- n)} by H2;
A3: for n being Nat holds (Partial_Union A1) . n is Event of Borel_Sets

proof

defpred S₁[ Nat] means (Partial_Union A1) . $1 in Borel_Sets ;
B0: (Partial_Union A1) . 0 = A1 . 0 by PROB_3:def 2;
A1 . 0 = {0} by A1;
then J0: S₁[ 0 ] by Th1, B0;
J1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume Q0: S₁[n] ; :: thesis: S₁[n + 1]
(Partial_Union A1) . (n + 1) in Borel_Sets

proof

C0: (Partial_Union A1) . (n + 1) = ((Partial_Union A1) . n) \/ (A1 . (n + 1)) by PROB_3:def 2;
C2: A1 . (n + 1) in Borel_Sets

proof

A1 . (n + 1) = {(n + 1)} by A1;
hence A1 . (n + 1) in Borel_Sets by Th1; :: thesis: verum

end;

((Partial_Union A1) . n) \/ (A1 . (n + 1)) is Event of Borel_Sets by Q0, C2, PROB_1:21;
hence (Partial_Union A1) . (n + 1) in Borel_Sets by C0; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(J0, J1);
hence for n being Nat holds (Partial_Union A1) . n is Event of Borel_Sets ; :: thesis: verum

end;

defpred S₁[ Nat] means (Partial_Union A2) . $1 in Borel_Sets ;
B0: (Partial_Union A2) . 0 = A2 . 0 by PROB_3:def 2;
A2 . 0 = {(- 0)} by A2;
then J0: S₁[ 0 ] by Th1, B0;
A4: for n being Nat holds (Partial_Union A2) . n is Event of Borel_Sets

proof

J1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume Q0: S₁[n] ; :: thesis: S₁[n + 1]
(Partial_Union A2) . (n + 1) in Borel_Sets

proof

C0: (Partial_Union A2) . (n + 1) = ((Partial_Union A2) . n) \/ (A2 . (n + 1)) by PROB_3:def 2;
A2 . (n + 1) = {(- (n + 1))} by A2;
then A2 . (n + 1) in Borel_Sets by Th1;
then ((Partial_Union A2) . n) \/ (A2 . (n + 1)) is Event of Borel_Sets by Q0, PROB_1:21;
hence (Partial_Union A2) . (n + 1) in Borel_Sets by C0; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(J0, J1);
hence for n being Nat holds (Partial_Union A2) . n is Event of Borel_Sets ; :: thesis: verum

end;

consider B1 being SetSequence of REAL such that
A5: for n being Nat holds B1 . n = (Partial_Union A1) . n by ThA;
A6: for n being Nat holds B1 . n is Event of Borel_Sets

proof

let n be Nat; :: thesis: B1 . n is Event of Borel_Sets
(Partial_Union A1) . n is Event of Borel_Sets by A3;
hence B1 . n is Event of Borel_Sets by A5; :: thesis: verum

end;

consider B2 being SetSequence of REAL such that
A7: for n being Nat holds B2 . n = (Partial_Union A2) . n by ThA;
A8: for n being Nat holds B2 . n is Event of Borel_Sets

proof

let n be Nat; :: thesis: B2 . n is Event of Borel_Sets
(Partial_Union A2) . n is Event of Borel_Sets by A4;
hence B2 . n is Event of Borel_Sets by A7; :: thesis: verum

end;

reconsider B1 = B1 as SetSequence of Borel_Sets by A6, PROB_1:25;
reconsider B2 = B2 as SetSequence of Borel_Sets by A8, PROB_1:25;
A9: Union B1 is Event of Borel_Sets by PROB_1:26;
A10: Union B2 is Event of Borel_Sets by PROB_1:26;
(Union B1) \/ (Union B2) = INT

proof

for x being object holds
( x in (Union B1) \/ (Union B2) iff x in INT )

proof

let x be object ; :: thesis: ( x in (Union B1) \/ (Union B2) iff x in INT )
thus ( x in (Union B1) \/ (Union B2) implies x in INT ) :: thesis: ( x in INT implies x in (Union B1) \/ (Union B2) )

proof

assume x in (Union B1) \/ (Union B2) ; :: thesis: x in INT

per cases then ( x in Union B1 or x in Union B2 ) by XBOOLE_0:def 3;

suppose F0: x in Union B1 ; :: thesis: x in INT

consider n being Nat such that
F1: x in B1 . n by F0, PROB_1:12;
F2: x in (Partial_Union A1) . n by F1, A5;
consider k being Nat such that
G1: ( k <= n & x in (Partial_Union A1) . k ) by F2;
consider m being Nat such that
I0: ( m <= k & x in A1 . m ) by G1, PROB_3:13;
x in INT

proof

x in {m} by I0, A1;
then I1: x = m by TARSKI:def 1;
m + 0 in NAT ;
hence x in INT by I1, NUMBERS:17; :: thesis: verum

end;

hence x in INT ; :: thesis: verum

end;

suppose x in Union B2 ; :: thesis: x in INT

then consider k being Nat such that
H1: x in B2 . k by PROB_1:12;
x in (Partial_Union A2) . k by H1, A7;
then consider z being Nat such that
G1: ( z <= k & x in A2 . z ) by PROB_3:13;
x in {(- z)} by G1, A2;
then x = - z by TARSKI:def 1;
hence x in INT by INT_1:def 1; :: thesis: verum

end;

end;

end;

( x in INT implies x in (Union B1) \/ (Union B2) )

proof

assume x in INT ; :: thesis: x in (Union B1) \/ (Union B2)
then consider k being Nat such that
E0: ( x = k or x = - k ) by INT_1:def 1;

per cases ( x = k or x = - k ) by E0;

suppose x = k ; :: thesis: x in (Union B1) \/ (Union B2)

then reconsider p2 = x as Nat ;
x in (Union B1) \/ (Union B2)

proof

ex k being Nat st x in B1 . k

proof

ex q being Nat st x in (Partial_Union A1) . q

proof

x in {p2} by TARSKI:def 1;
then x in A1 . p2 by A1;
then x in (Partial_Union A1) . p2 by PROB_3:13;
hence ex q being Nat st x in (Partial_Union A1) . q ; :: thesis: verum

end;

then consider q being Nat such that
I0: x in (Partial_Union A1) . q ;
B1 . q = (Partial_Union A1) . q by A5;
hence ex k being Nat st x in B1 . k by I0; :: thesis: verum

end;

then x in Union B1 by PROB_1:12;
hence x in (Union B1) \/ (Union B2) by XBOOLE_0:def 3; :: thesis: verum

end;

hence x in (Union B1) \/ (Union B2) ; :: thesis: verum

end;

suppose F1: x = - k ; :: thesis: x in (Union B1) \/ (Union B2)

- k is Element of INT by INT_1:def 1;
then consider z being Element of INT such that
G0: ( z = - k & - k = x ) by F1;
x in (Union B1) \/ (Union B2)

proof

ex k being Nat st x in B2 . k

proof

ex q being Nat st x in (Partial_Union A2) . q

proof

K0: x in {(- k)} by G0, TARSKI:def 1;
x in A2 . k by A2, K0;
then x in (Partial_Union A2) . k by PROB_3:13;
then consider q being Nat such that
I0: x in (Partial_Union A2) . q ;
thus ex q being Nat st x in (Partial_Union A2) . q by I0; :: thesis: verum

end;

then consider q being Nat such that
I0: x in (Partial_Union A2) . q ;
B2 . q = (Partial_Union A2) . q by A7;
hence ex k being Nat st x in B2 . k by I0; :: thesis: verum

end;

then ( x in Union B2 or x in Union B2 ) by PROB_1:12;
hence x in (Union B1) \/ (Union B2) by XBOOLE_0:def 3; :: thesis: verum

end;

hence x in (Union B1) \/ (Union B2) ; :: thesis: verum

end;

end;

end;

hence ( x in INT implies x in (Union B1) \/ (Union B2) ) ; :: thesis: verum

end;

hence (Union B1) \/ (Union B2) = INT ; :: thesis: verum

end;

hence INT is Event of Borel_Sets by A9, A10, PROB_1:3; :: thesis: verum