let a, b, c, d be Real; :: thesis: ( 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 ; :: 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);
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:54;
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:44
.= ((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:36
.= ((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
.= inside_of_rectangle (a,b,c,d) by Th49 ; :: thesis: verum