let a, b, c, d be Real; :: thesis: (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; :: according to XBOOLE_0:def 10 :: thesis: 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)) ; :: thesis: verum