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 and
A3: p `1 <= b and
A4: c <= p `2 and
A5: 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, A3, A4, A5; :: 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 A6: x in (outside_of_rectangle a,b,c,d) ` ; :: thesis: x in closed_inside_of_rectangle a,b,c,d
then A7: 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 A6;
A8: a <= x `1 by A7;
A9: x `1 <= b by A7;
A10: c <= x `2 by A7;
x `2 <= d by A7;
hence x in closed_inside_of_rectangle a,b,c,d by A8, A9, A10; :: thesis: verum