let a, b, c, d be real number ; :: thesis: ( a < b & c < d implies Int (closed_inside_of_rectangle a,b,c,d) = inside_of_rectangle a,b,c,d )
assume A1: ( a < b & c < d ) ; :: thesis: 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;
A2: ( a is Real & b is Real & c is Real & d is Real ) by XREAL_0:def 1;
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, SPPOL_2:58;
A4: 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, 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, 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 A4, XBOOLE_0:def 7
.= inside_of_rectangle a,b,c,d by Th49 ; :: thesis: verum