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:18;
then A1: [:[.a,b.],[.c,d.]:] c= [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:96;
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 2;
( [.a,b.] is compact Subset of I[01] & [.c,d.] is compact Subset of I[01] ) by A2, BORSUK_4:24;
then Ewa is compact Subset of [:I[01],I[01]:] by BORSUK_3:23;
hence [:[.a,b.],[.c,d.]:] is non empty compact Subset of [:I[01],I[01]:] ; :: thesis: verum