let a, b, c, d be Point of I[01] ; :: thesis: ( a <= b & c <= d implies [:[.a,b.],[.c,d.]:] is non empty compact Subset of [:I[01] ,I[01] :] )
assume that
A1: a <= b and
A2: c <= d ; :: thesis: [:[.a,b.],[.c,d.]:] is non empty compact Subset of [:I[01] ,I[01] :]
A3: [.a,b.] is Subset of I[01] by BORSUK_4:43;
[.c,d.] is Subset of I[01] by BORSUK_4:43;
then A4: [:[.a,b.],[.c,d.]:] c= [:the carrier of I[01] ,the carrier of I[01] :] by A3, ZFMISC_1:119;
A5: a in [.a,b.] by A1, XXREAL_1:1;
c in [.c,d.] by A2, XXREAL_1:1;
then reconsider Ewa = [:[.a,b.],[.c,d.]:] as non empty Subset of [:I[01] ,I[01] :] by A4, A5, BORSUK_1:def 5;
( [.a,b.] is compact Subset of I[01] & [.c,d.] is compact Subset of I[01] ) by A1, A2, BORSUK_4:49;
then Ewa is compact Subset of [:I[01] ,I[01] :] by BORSUK_3:27;
hence [:[.a,b.],[.c,d.]:] is non empty compact Subset of [:I[01] ,I[01] :] ; :: thesis: verum