let a, b, c, d be real number ; :: thesis: ( a <= b & c <= d implies (closed_inside_of_rectangle a,b,c,d) \ (inside_of_rectangle a,b,c,d) = rectangle a,b,c,d )
assume A1: ( a <= b & c <= d ) ; :: thesis: (closed_inside_of_rectangle a,b,c,d) \ (inside_of_rectangle a,b,c,d) = rectangle a,b,c,d
set R = rectangle a,b,c,d;
set P = closed_inside_of_rectangle a,b,c,d;
set P1 = inside_of_rectangle a,b,c,d;
A2: rectangle a,b,c,d = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = a & p `2 <= d & p `2 >= c ) or ( p `1 <= b & p `1 >= a & p `2 = d ) or ( p `1 <= b & p `1 >= a & p `2 = c ) or ( p `1 = b & p `2 <= d & p `2 >= c ) ) } by A1, SPPOL_2:58;
thus (closed_inside_of_rectangle a,b,c,d) \ (inside_of_rectangle a,b,c,d) c= rectangle a,b,c,d :: according to XBOOLE_0:def 10 :: thesis: rectangle a,b,c,d c= (closed_inside_of_rectangle a,b,c,d) \ (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) \ (inside_of_rectangle a,b,c,d) or x in rectangle a,b,c,d )
assume A3: x in (closed_inside_of_rectangle a,b,c,d) \ (inside_of_rectangle a,b,c,d) ; :: thesis: x in rectangle a,b,c,d
then A4: not x in inside_of_rectangle a,b,c,d by XBOOLE_0:def 5;
x in closed_inside_of_rectangle a,b,c,d by A3, XBOOLE_0:def 5;
then consider p being Point of (TOP-REAL 2) such that
A5: x = p and
A6: ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) ;
( not a < p `1 or not p `1 < b or not c < p `2 or not p `2 < d ) by A4, A5;
then ( ( p `1 = a & p `2 <= d & p `2 >= c ) or ( p `1 <= b & p `1 >= a & p `2 = d ) or ( p `1 <= b & p `1 >= a & p `2 = c ) or ( p `1 = b & p `2 <= d & p `2 >= c ) ) by A6, XXREAL_0:1;
hence x in rectangle a,b,c,d by A2, A5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rectangle a,b,c,d or x in (closed_inside_of_rectangle a,b,c,d) \ (inside_of_rectangle a,b,c,d) )
assume A7: x in rectangle a,b,c,d ; :: thesis: x in (closed_inside_of_rectangle a,b,c,d) \ (inside_of_rectangle a,b,c,d)
then A8: ex p being Point of (TOP-REAL 2) st
( p = x & ( ( p `1 = a & p `2 <= d & p `2 >= c ) or ( p `1 <= b & p `1 >= a & p `2 = d ) or ( p `1 <= b & p `1 >= a & p `2 = c ) or ( p `1 = b & p `2 <= d & p `2 >= c ) ) ) by A2;
A9: rectangle a,b,c,d c= closed_inside_of_rectangle a,b,c,d by A1, Th45;

now

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

end;

hence x in (closed_inside_of_rectangle a,b,c,d) \ (inside_of_rectangle a,b,c,d) by A7, A9, XBOOLE_0:def 5; :: thesis: verum