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