let r, s be Real; for F being Subset-Family of (Closed-Interval-TSpace (r,s))
for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & len C = 1 holds
C = <*[.r,s.]*>
let F be Subset-Family of (Closed-Interval-TSpace (r,s)); for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & len C = 1 holds
C = <*[.r,s.]*>
let C be IntervalCover of F; ( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & len C = 1 implies C = <*[.r,s.]*> )
assume that
A1:
( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s )
and
A2:
len C = 1
; C = <*[.r,s.]*>
A3:
union (rng C) = [.r,s.]
by A1, Def2;
not C is empty
by A2;
then
not rng C is empty
;
then
1 in dom C
by FINSEQ_3:32;
then A4:
C . 1 in rng C
by FUNCT_1:def 3;
C . 1 = [.r,s.]
proof
thus
for
a being
object st
a in C . 1 holds
a in [.r,s.]
by A3, A4, TARSKI:def 4;
TARSKI:def 3,
XBOOLE_0:def 10 [.r,s.] c= C . 1
let a be
object ;
TARSKI:def 3 ( not a in [.r,s.] or a in C . 1 )
A5:
dom C = {1}
by A2, FINSEQ_1:2, FINSEQ_1:def 3;
assume
a in [.r,s.]
;
a in C . 1
then consider Z being
set such that A6:
a in Z
and A7:
Z in rng C
by A3, TARSKI:def 4;
ex
x being
object st
(
x in dom C &
C . x = Z )
by A7, FUNCT_1:def 3;
hence
a in C . 1
by A6, A5, TARSKI:def 1;
verum
end;
hence
C = <*[.r,s.]*>
by A2, FINSEQ_1:40; verum