let r, s be Real; for F being Subset-Family of (Closed-Interval-TSpace (r,s))
for C being IntervalCover of F
for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & len C = 1 holds
G = <*r,s*>
let F be Subset-Family of (Closed-Interval-TSpace (r,s)); for C being IntervalCover of F
for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & len C = 1 holds
G = <*r,s*>
let C be IntervalCover of F; for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & len C = 1 holds
G = <*r,s*>
let G be IntervalCoverPts of C; ( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & len C = 1 implies G = <*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
; G = <*r,s*>
A3:
G . 1 = r
by A1, Def3;
A4:
len G = (len C) + 1
by A1, Def3;
then
G . 2 = s
by A1, A2, Def3;
hence
G = <*r,s*>
by A2, A4, A3, FINSEQ_1:44; verum