set P2 = outside_of_rectangle (a,b,c,d);
A1: a is Real by XREAL_0:def 1;
A2: b is Real by XREAL_0:def 1;
A3: c is Real by XREAL_0:def 1;
d is Real by XREAL_0:def 1;
then reconsider P2 = outside_of_rectangle (a,b,c,d) as open Subset of (TOP-REAL 2) by A1, A2, A3, JORDAN1:34;
P2 ` is closed ;
hence closed_inside_of_rectangle (a,b,c,d) is closed by Th47; :: thesis: verum