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:39;
P2 ` is closed ;
hence closed_inside_of_rectangle a,b,c,d is closed by Th47; :: thesis: verum