set P2 = outside_of_rectangle a,b,c,d;
( a is Real & b is Real & c is Real & 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 JORDAN1:39;
P2 ` is closed ;
hence closed_inside_of_rectangle a,b,c,d is closed by Th47; :: thesis: verum