let r, s be real number ; :: thesis: 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); :: thesis: 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; :: thesis: 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; :: thesis: ( 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) and
A2: F is open and
A3: F is connected and
A4: r <= s and
A5: len C = 1 ; :: thesis: G = <*r,s*>
A6: len G = (len C) + 1 by A1, A2, A3, A4, Def3;
then ( G . 1 = r & G . 2 = s ) by A1, A2, A3, A4, A5, Def3;
hence G = <*r,s*> by A5, A6, FINSEQ_1:61; :: thesis: verum