let a, b, c, d be real number ; :: 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 set 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