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

not G is empty

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

not G is empty

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

not G is empty

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 not G is empty )

assume ( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s ) ; :: thesis: not G is empty

then len G = (len C) + 1 by RCOMP_3:def 3;

hence not G is empty by CARD_1:27; :: thesis: verum

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

not G is empty

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

not G is empty

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

not G is empty

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 not G is empty )

assume ( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s ) ; :: thesis: not G is empty

then len G = (len C) + 1 by RCOMP_3:def 3;

hence not G is empty by CARD_1:27; :: thesis: verum