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

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;