let a, b, c, d be Real; :: thesis: closed_inside_of_rectangle (a,b,c,d) misses outside_of_rectangle (a,b,c,d)
set R = closed_inside_of_rectangle (a,b,c,d);
set P2 = outside_of_rectangle (a,b,c,d);
assume closed_inside_of_rectangle (a,b,c,d) meets outside_of_rectangle (a,b,c,d) ; :: thesis: contradiction
then consider x being object such that
A1: x in closed_inside_of_rectangle (a,b,c,d) and
A2: x in outside_of_rectangle (a,b,c,d) by XBOOLE_0:3;
A3: ex p being Point of (TOP-REAL 2) st
( x = p & a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) by A1;
ex p being Point of (TOP-REAL 2) st
( x = p & ( not a <= p `1 or not p `1 <= b or not c <= p `2 or not p `2 <= d ) ) by A2;
hence contradiction by A3; :: thesis: verum