let a, b, c, d be Point of ; :: thesis: ( a <= b & c <= d implies [:[.a,b.],[.c,d.]:] is non empty compact Subset of )
( [.a,b.] is Subset of & [.c,d.] is Subset of ) 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
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 by A1, BORSUK_1:def 5;
( [.a,b.] is compact Subset of & [.c,d.] is compact Subset of ) by A2, BORSUK_4:49;
then Ewa is compact Subset of by BORSUK_3:27;
hence [:[.a,b.],[.c,d.]:] is non empty compact Subset of ; :: thesis: verum