let a, b, c, d be real number ; ( a < b & c < d implies Int (closed_inside_of_rectangle a,b,c,d) = inside_of_rectangle a,b,c,d )
assume that
A1:
a < b
and
A2:
c < d
; Int (closed_inside_of_rectangle a,b,c,d) = inside_of_rectangle a,b,c,d
set P = rectangle a,b,c,d;
set R = closed_inside_of_rectangle a,b,c,d;
set P1 = inside_of_rectangle a,b,c,d;
set P2 = outside_of_rectangle a,b,c,d;
A3:
a is Real
by XREAL_0:def 1;
A4:
b is Real
by XREAL_0:def 1;
A5:
c is Real
by XREAL_0:def 1;
A6:
d is Real
by XREAL_0:def 1;
A7:
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;
A8:
closed_inside_of_rectangle a,b,c,d misses outside_of_rectangle a,b,c,d
by Th48;
thus Int (closed_inside_of_rectangle a,b,c,d) =
(Cl (((outside_of_rectangle a,b,c,d) ` ) ` )) `
by Th47
.=
((outside_of_rectangle a,b,c,d) \/ (rectangle a,b,c,d)) `
by A1, A2, A3, A4, A5, A6, A7, JORDAN1:49
.=
((outside_of_rectangle a,b,c,d) ` ) /\ ((rectangle a,b,c,d) ` )
by XBOOLE_1:53
.=
(closed_inside_of_rectangle a,b,c,d) /\ ((rectangle a,b,c,d) ` )
by Th47
.=
(closed_inside_of_rectangle a,b,c,d) /\ ((inside_of_rectangle a,b,c,d) \/ (outside_of_rectangle a,b,c,d))
by A1, A2, A3, A4, A5, A6, A7, JORDAN1:41
.=
((closed_inside_of_rectangle a,b,c,d) /\ (inside_of_rectangle a,b,c,d)) \/ ((closed_inside_of_rectangle a,b,c,d) /\ (outside_of_rectangle a,b,c,d))
by XBOOLE_1:23
.=
((closed_inside_of_rectangle a,b,c,d) /\ (inside_of_rectangle a,b,c,d)) \/ {}
by A8, XBOOLE_0:def 7
.=
inside_of_rectangle a,b,c,d
by Th49
; verum