let r, s be Real; :: 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 holds
2 <= len G
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 holds
2 <= len G
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 holds
2 <= len G
let G be IntervalCoverPts of C; :: thesis: ( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s implies 2 <= len G )
assume A1: ( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s ) ; :: thesis: 2 <= len G
then 1 <= len C by Th51;
then 1 + 1 <= (len C) + 1 by XREAL_1:6;
hence 2 <= len G by A1, Def3; :: thesis: verum