let a, b, c, d be real number ; :: thesis: closed_inside_of_rectangle a,b,c,d = (outside_of_rectangle a,b,c,d) `
set R = closed_inside_of_rectangle a,b,c,d;
set O = outside_of_rectangle a,b,c,d;
thus closed_inside_of_rectangle a,b,c,d c= (outside_of_rectangle a,b,c,d) ` :: according to XBOOLE_0:def 10 :: thesis: (outside_of_rectangle a,b,c,d) ` c= closed_inside_of_rectangle a,b,c,d

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in closed_inside_of_rectangle a,b,c,d or x in (outside_of_rectangle a,b,c,d) ` )
assume x in closed_inside_of_rectangle a,b,c,d ; :: thesis: x in (outside_of_rectangle a,b,c,d) `
then consider p being Point of (TOP-REAL 2) such that
A1: x = p and
A2: ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) ;

now

assume p in outside_of_rectangle a,b,c,d ; :: thesis: contradiction
then ex p1 being Point of (TOP-REAL 2) st
( p1 = p & ( not a <= p1 `1 or not p1 `1 <= b or not c <= p1 `2 or not p1 `2 <= d ) ) ;
hence contradiction by A2; :: thesis: verum

end;

hence x in (outside_of_rectangle a,b,c,d) ` by A1, SUBSET_1:50; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (outside_of_rectangle a,b,c,d) ` or x in closed_inside_of_rectangle a,b,c,d )
assume A3: x in (outside_of_rectangle a,b,c,d) ` ; :: thesis: x in closed_inside_of_rectangle a,b,c,d
then A4: not x in outside_of_rectangle a,b,c,d by XBOOLE_0:def 5;
reconsider x = x as Point of (TOP-REAL 2) by A3;
( a <= x `1 & x `1 <= b & c <= x `2 & x `2 <= d ) by A4;
hence x in closed_inside_of_rectangle a,b,c,d ; :: thesis: verum