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] :] )
( [.a,b.] is Subset of I[01] & [.c,d.] is Subset of I[01] ) by BORSUK_4:43;
then A1: [:[.a,b.],[.c,d.]:] c= [:the carrier of I[01] ,the carrier of I[01] :] by ZFMISC_1:119;
assume A2: ( a <= b & c <= d ) ; :: thesis: [:[.a,b.],[.c,d.]:] is non empty compact Subset of [:I[01] ,I[01] :]
then ( a in [.a,b.] & c in [.c,d.] ) by XXREAL_1:1;
then reconsider Ewa = [:[.a,b.],[.c,d.]:] as non empty Subset of [:I[01] ,I[01] :] by A1, BORSUK_1:def 5;
( [.a,b.] is compact Subset of I[01] & [.c,d.] is compact Subset of I[01] ) by 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