let a, b, c, d be Real; (closed_inside_of_rectangle (a,b,c,d)) /\ (inside_of_rectangle (a,b,c,d)) = inside_of_rectangle (a,b,c,d)
set R = closed_inside_of_rectangle (a,b,c,d);
set P1 = inside_of_rectangle (a,b,c,d);
thus
(closed_inside_of_rectangle (a,b,c,d)) /\ (inside_of_rectangle (a,b,c,d)) c= inside_of_rectangle (a,b,c,d)
by XBOOLE_1:17; XBOOLE_0:def 10 inside_of_rectangle (a,b,c,d) c= (closed_inside_of_rectangle (a,b,c,d)) /\ (inside_of_rectangle (a,b,c,d))
(inside_of_rectangle (a,b,c,d)) /\ (inside_of_rectangle (a,b,c,d)) c= (inside_of_rectangle (a,b,c,d)) /\ (closed_inside_of_rectangle (a,b,c,d))
by Th46, XBOOLE_1:26;
hence
inside_of_rectangle (a,b,c,d) c= (closed_inside_of_rectangle (a,b,c,d)) /\ (inside_of_rectangle (a,b,c,d))
; verum