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 that
A1: a <= b and
A2: 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;
A3: 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, A2, 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 A4: 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 A5: 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 A4, XBOOLE_0:def 5;
then consider p being Point of (TOP-REAL 2) such that
A6: x = p and
A7: a <= p `1 and
A8: p `1 <= b and
A9: c <= p `2 and
A10: p `2 <= d ;
( not a < p `1 or not p `1 < b or not c < p `2 or not p `2 < d ) by A5, A6;
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 A7, A8, A9, A10, XXREAL_0:1;
hence x in rectangle a,b,c,d by A3, A6; :: 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 A11: 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 A12: 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 A3;
A13: rectangle a,b,c,d c= closed_inside_of_rectangle a,b,c,d by A1, A2, 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 A12; :: thesis: verum

end;

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