let r, s be real number ; :: thesis: 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 holds
1 <= len C
let F be Subset-Family of (Closed-Interval-TSpace r,s); :: thesis: for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace r,s) & F is open & F is connected & r <= s holds
1 <= len C
let C be IntervalCover of F; :: thesis: ( F is Cover of (Closed-Interval-TSpace r,s) & F is open & F is connected & r <= s implies 1 <= len C )
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 ; :: thesis: 1 <= len C
A5: union (rng C) = [.r,s.] by A1, A2, A3, A4, Def2;
assume not 1 <= len C ; :: thesis: contradiction
then (len C) + 1 <= 0 + 1 by NAT_1:13;
then len C <= 0 by XREAL_1:8;
then len C = 0 ;
then C is empty ;
hence contradiction by A4, A5, RELAT_1:60, XXREAL_1:1, ZFMISC_1:2; :: thesis: verum