let a, b, c, d be Point of I[01] ; :: thesis: [:[.a,b.],[.c,d.]:] is compact Subset of [:I[01] ,I[01] :]

per cases ( ( a <= b & c <= d ) or ( a > b & c <= d ) or ( a > b & c > d ) or ( a <= b & c > d ) ) ;

suppose ( a <= b & c <= d ) ; :: thesis: [:[.a,b.],[.c,d.]:] is compact Subset of [:I[01] ,I[01] :]

hence [:[.a,b.],[.c,d.]:] is compact Subset of [:I[01] ,I[01] :] by Th13; :: thesis: verum

end;

suppose ( a > b & c <= d ) ; :: thesis: [:[.a,b.],[.c,d.]:] is compact Subset of [:I[01] ,I[01] :]

then reconsider A = [.a,b.] as empty Subset of I[01] by Th35;
[:A,[.c,d.]:] = {} ;
hence [:[.a,b.],[.c,d.]:] is compact Subset of [:I[01] ,I[01] :] by Th34; :: thesis: verum

end;

suppose ( a > b & c > d ) ; :: thesis: [:[.a,b.],[.c,d.]:] is compact Subset of [:I[01] ,I[01] :]

then reconsider A = [.c,d.] as empty Subset of I[01] by Th35;
[:[.a,b.],A:] = {} ;
hence [:[.a,b.],[.c,d.]:] is compact Subset of [:I[01] ,I[01] :] by Th34; :: thesis: verum

end;

suppose ( a <= b & c > d ) ; :: thesis: [:[.a,b.],[.c,d.]:] is compact Subset of [:I[01] ,I[01] :]

then reconsider A = [.c,d.] as empty Subset of I[01] by Th35;
[:[.a,b.],A:] = {} ;
hence [:[.a,b.],[.c,d.]:] is compact Subset of [:I[01] ,I[01] :] by Th34; :: thesis: verum

end;

end;