theorem Th47: :: JORDAN:47

for a, b, c, d being Real holds closed_inside_of_rectangle (a,b,c,d) = (outside_of_rectangle (a,b,c,d)) `