let F be non empty disjoint_valued FinSequence of Family_of_Intervals ; :: thesis: ( Union F is Interval implies ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval ) )
assume A1: Union F is Interval ; :: thesis: ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval )
then reconsider UF = Union F as Interval ;
A2: Union F = union (rng F) by CARD_3:def 4;

per cases ( Union F = {} or Union F is non empty closed_interval Subset of REAL or Union F is non empty left_open_interval Subset of REAL or Union F is non empty right_open_interval Subset of REAL or Union F is non empty open_interval Subset of REAL ) by A1, MEASURE5:1;

suppose A3: Union F = {} ; :: thesis: ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval )

A4: rng F <> {} ;
( (Union F) \ (F . 1) = {} & {} c= REAL ) by A3;
hence ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval ) by A4, FINSEQ_3:32; :: thesis: verum

end;

suppose A5: Union F is non empty closed_interval Subset of REAL ; :: thesis: ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval )

then A6: Union F = [.(inf UF),(sup UF).] by MEASURE6:17;
then inf UF <= sup UF by A5, XXREAL_1:29;
then inf UF in Union F by A6, XXREAL_1:1;
then consider A being set such that
A7: ( inf UF in A & A in rng F ) by A2, TARSKI:def 4;
consider n being Element of NAT such that
A8: ( n in dom F & A = F . n ) by A7, PARTFUN1:3;
A9: ( inf UF <= inf (F . n) & sup (F . n) <= sup UF ) by A2, A7, A8, ZFMISC_1:74, XXREAL_2:59, XXREAL_2:60;
inf (F . n) is LowerBound of F . n by XXREAL_2:def 4;
then inf (F . n) <= inf UF by A7, A8, XXREAL_2:def 2;
then A10: inf UF = inf (F . n) by A9, XXREAL_0:1;
then A11: F . n is left_end by A7, A8, XXREAL_2:def 5;

per cases ( F . n is right_end or not F . n is right_end ) ;

suppose F . n is right_end ; :: thesis: ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval )

then F . n = [.(inf (F . n)),(sup (F . n)).] by A11, XXREAL_2:75;
then (Union F) \ (F . n) = ].(sup (F . n)),(sup UF).] by A6, A7, A8, XXREAL_2:40, A10, XXREAL_1:182;
then UF \ (F . n) is interval Subset of REAL ;
hence ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval ) by A8; :: thesis: verum

end;

suppose not F . n is right_end ; :: thesis: ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval )

then F . n = [.(inf (F . n)),(sup (F . n)).[ by A11, XXREAL_2:77;
then (Union F) \ (F . n) = [.(sup (F . n)),(sup UF).] by A6, A10, A7, A8, XXREAL_1:27, XXREAL_1:184;
then UF \ (F . n) is interval Subset of REAL ;
hence ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval ) by A8; :: thesis: verum

end;

end;

end;

suppose A12: Union F is non empty left_open_interval Subset of REAL ; :: thesis: ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval )

then A13: Union F = ].(inf UF),(sup UF).] by MEASURE6:19;
then sup UF in Union F by A12, XXREAL_1:26, XXREAL_1:2;
then consider A being set such that
A14: ( sup UF in A & A in rng F ) by A2, TARSKI:def 4;
consider n being Element of NAT such that
A15: ( n in dom F & A = F . n ) by A14, PARTFUN1:3;
A16: ( inf UF <= inf (F . n) & sup (F . n) <= sup UF ) by A2, A14, A15, ZFMISC_1:74, XXREAL_2:59, XXREAL_2:60;
sup (F . n) is UpperBound of F . n by XXREAL_2:def 3;
then sup (F . n) >= sup UF by A14, A15, XXREAL_2:def 1;
then A17: sup UF = sup (F . n) by A16, XXREAL_0:1;
then A18: F . n is right_end by A14, A15, XXREAL_2:def 6;

per cases ( F . n is left_end or not F . n is left_end ) ;

suppose F . n is left_end ; :: thesis: ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval )

then F . n = [.(inf (F . n)),(sup (F . n)).] by A18, XXREAL_2:75;
then (Union F) \ (F . n) = ].(inf UF),(inf (F . n)).[ by A13, A14, A15, XXREAL_2:40, A17, XXREAL_1:191;
hence ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval ) by A15; :: thesis: verum

end;

suppose not F . n is left_end ; :: thesis: ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval )

then F . n = ].(inf (F . n)),(sup (F . n)).] by A18, XXREAL_2:76;
then (Union F) \ (F . n) = ].(inf UF),(inf (F . n)).] by A13, A17, A14, A15, XXREAL_1:26, XXREAL_1:193;
then UF \ (F . n) is interval Subset of REAL ;
hence ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval ) by A15; :: thesis: verum

end;

end;

end;

suppose A19: Union F is non empty right_open_interval Subset of REAL ; :: thesis: ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval )

then A20: Union F = [.(inf UF),(sup UF).[ by MEASURE6:18;
then inf UF in Union F by A19, XXREAL_1:27, XXREAL_1:3;
then consider A being set such that
A21: ( inf UF in A & A in rng F ) by A2, TARSKI:def 4;
consider n being Element of NAT such that
A22: ( n in dom F & A = F . n ) by A21, PARTFUN1:3;
A23: ( inf UF <= inf (F . n) & sup (F . n) <= sup UF ) by A2, A21, A22, ZFMISC_1:74, XXREAL_2:59, XXREAL_2:60;
inf (F . n) is LowerBound of F . n by XXREAL_2:def 4;
then inf (F . n) <= inf UF by A21, A22, XXREAL_2:def 2;
then A24: inf UF = inf (F . n) by A23, XXREAL_0:1;
then A25: F . n is left_end by A21, A22, XXREAL_2:def 5;

per cases ( F . n is right_end or not F . n is right_end ) ;

suppose F . n is right_end ; :: thesis: ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval )

then F . n = [.(inf (F . n)),(sup (F . n)).] by A25, XXREAL_2:75;
then (Union F) \ (F . n) = ].(sup (F . n)),(sup UF).[ by A20, A21, A22, XXREAL_2:40, A24, XXREAL_1:183;
hence ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval ) by A22; :: thesis: verum

end;

suppose not F . n is right_end ; :: thesis: ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval )

then F . n = [.(inf (F . n)),(sup (F . n)).[ by A25, XXREAL_2:77;
then (Union F) \ (F . n) = [.(sup (F . n)),(sup UF).[ by A20, A24, A21, A22, XXREAL_1:27, XXREAL_1:185;
then UF \ (F . n) is interval Subset of REAL ;
hence ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval ) by A22; :: thesis: verum

end;

end;

end;

suppose A26: Union F is non empty open_interval Subset of REAL ; :: thesis: ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval )

then A27: Union F = ].(inf UF),(sup UF).[ by MEASURE6:16;
deffunc H₁( Nat) -> Element of ExtREAL = inf (F . $1);
consider G being FinSequence of ExtREAL such that
A28: ( len G = len F & ( for n being Nat st n in dom G holds
G . n = H₁(n) ) ) from FINSEQ_2:sch 1();
A29: min_p G in dom G by A28, Def2;
A30: for n being Nat st n in dom F holds
inf (F . (min_p G)) <= inf (F . n)

proof

let n be Nat; :: thesis: ( n in dom F implies inf (F . (min_p G)) <= inf (F . n) )
assume A31: n in dom F ; :: thesis: inf (F . (min_p G)) <= inf (F . n)
then ( 1 <= n & n <= len G ) by A28, FINSEQ_3:25;
then A32: ( G . (min_p G) <= G . n & min G <= G . n ) by Th26;
min_p G in dom G by A28, Def2;
then A33: G . (min_p G) = inf (F . (min_p G)) by A28;
n in dom G by A28, A31, FINSEQ_3:29;
hence inf (F . (min_p G)) <= inf (F . n) by A32, A33, A28; :: thesis: verum

end;

A34: min_p G in dom F by A29, A28, FINSEQ_3:29;
then F . (min_p G) c= UF by A2, ZFMISC_1:74, FUNCT_1:3;
then A35: ( inf UF <= inf (F . (min_p G)) & sup (F . (min_p G)) <= sup UF ) by XXREAL_2:59, XXREAL_2:60;

A36: now :: thesis: not inf (F . (min_p G)) = +infty

assume A37: inf (F . (min_p G)) = +infty ; :: thesis: contradiction
A38: for n being Nat holds
( not n in dom F or F . n = {+infty} or F . n = {} )

proof

let n be Nat; :: thesis: ( not n in dom F or F . n = {+infty} or F . n = {} )
assume n in dom F ; :: thesis: ( F . n = {+infty} or F . n = {} )
then inf (F . n) = +infty by A30, A37, XXREAL_0:4;
then +infty is LowerBound of F . n by XXREAL_2:def 4;
hence ( F . n = {+infty} or F . n = {} ) by ZFMISC_1:33, XXREAL_2:52; :: thesis: verum

end;

per cases ( ex n being Nat st
( n in dom F & F . n = {+infty} ) or for n being Nat st n in dom F holds
F . n <> {+infty} ) ;

suppose ex n being Nat st
( n in dom F & F . n = {+infty} ) ; :: thesis: contradiction

then consider n being Nat such that
A39: ( n in dom F & F . n = {+infty} ) ;
{+infty} c= UF by A2, A39, FUNCT_1:3, ZFMISC_1:74;
then +infty in UF by ZFMISC_1:31;
hence contradiction ; :: thesis: verum

end;

suppose A40: for n being Nat st n in dom F holds
F . n <> {+infty} ; :: thesis: contradiction

then A41: for n being Nat st n in dom F holds
F . n = {} by A38;
for x being object holds
( x in rng F iff x = {} )

proof

let x be object ; :: thesis: ( x in rng F iff x = {} )

hereby :: thesis: ( x = {} implies x in rng F )

assume x in rng F ; :: thesis: x = {}
then ex n being Element of NAT st
( n in dom F & x = F . n ) by PARTFUN1:3;
hence x = {} by A40, A38; :: thesis: verum

end;

assume A42: x = {} ; :: thesis: x in rng F
rng F <> {} ;
then ( 1 in dom F & F . 1 = x ) by A41, A42, FINSEQ_3:32;
hence x in rng F by FUNCT_1:3; :: thesis: verum

end;

then rng F = {{}} by TARSKI:def 1;
hence contradiction by A26, A2; :: thesis: verum

end;

end;

end;

then A43: inf (F . (min_p G)) <= sup (F . (min_p G)) by XXREAL_2:38, XXREAL_2:40;
A44: rng F c= bool REAL by XBOOLE_1:1;

now :: thesis: not inf UF < inf (F . (min_p G))

assume inf UF < inf (F . (min_p G)) ; :: thesis: contradiction
then consider x being R_eal such that
A45: ( inf UF < x & x < inf (F . (min_p G)) & x in REAL ) by MEASURE5:2;
x < sup (F . (min_p G)) by A45, A43, XXREAL_0:2;
then x < sup UF by A35, XXREAL_0:2;
then x in UF by A45, XXREAL_2:83;
then consider A being set such that
A46: ( x in A & A in rng F ) by A2, TARSKI:def 4;
reconsider A = A as non empty Subset of REAL by A46, A44;
consider n being Element of NAT such that
A47: ( n in dom F & A = F . n ) by A46, PARTFUN1:3;
inf (F . (min_p G)) <= inf A by A30, A47;
then x < inf A by A45, XXREAL_0:2;
hence contradiction by A46, XXREAL_2:3; :: thesis: verum

end;

then A48: inf UF = inf (F . (min_p G)) by A35, XXREAL_0:1;

now :: thesis: not inf (F . (min_p G)) in F . (min_p G)

assume A49: inf (F . (min_p G)) in F . (min_p G) ; :: thesis: contradiction
F . (min_p G) in rng F by A34, FUNCT_1:3;
then inf UF in UF by A2, A48, A49, TARSKI:def 4;
hence contradiction by A27, XXREAL_1:4; :: thesis: verum

end;

then A50: not F . (min_p G) is left_end by XXREAL_2:def 5;

per cases ( F . (min_p G) is right_end or not F . (min_p G) is right_end ) ;

suppose F . (min_p G) is right_end ; :: thesis: ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval )

then F . (min_p G) = ].(inf (F . (min_p G))),(sup (F . (min_p G))).] by A50, XXREAL_2:76;
then (Union F) \ (F . (min_p G)) = ].(sup (F . (min_p G))),(sup UF).[ by A27, A48, A36, XXREAL_2:38, XXREAL_1:26, XXREAL_1:187;
hence ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval ) by A34; :: thesis: verum

end;

suppose not F . (min_p G) is right_end ; :: thesis: ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval )

then F . (min_p G) = ].(inf (F . (min_p G))),(sup (F . (min_p G))).[ by A50, A36, XXREAL_2:38, XXREAL_2:78;
then (Union F) \ (F . (min_p G)) = [.(sup (F . (min_p G))),(sup UF).[ by A27, A48, A36, XXREAL_2:38, XXREAL_1:28, XXREAL_1:189;
then UF \ (F . (min_p G)) is interval Subset of REAL ;
hence ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval ) by A34; :: thesis: verum

end;

end;

end;

end;