let a, b, c, d be real number ; :: 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