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 Th9; :: 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 Th31;
[:A,[.c,d.]:] = {} ;
hence [:[.a,b.],[.c,d.]:] is compact Subset of [:I[01],I[01]:] by Th30; :: 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 Th31;
[:[.a,b.],A:] = {} ;
hence [:[.a,b.],[.c,d.]:] is compact Subset of [:I[01],I[01]:] by Th30; :: 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 Th31;
[:[.a,b.],A:] = {} ;
hence [:[.a,b.],[.c,d.]:] is compact Subset of [:I[01],I[01]:] by Th30; :: thesis: verum

end;

end;