theorem Th57: :: JORDAN:57

for a, b, c, d being Real
for p1, p2 being Point of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) st a < b & c < d & p1 in closed_inside_of_rectangle (a,b,c,d) & not p2 in closed_inside_of_rectangle (a,b,c,d) & P is_an_arc_of p1,p2 holds
Segment (P,p1,p2,p1,(First_Point (P,p1,p2,(rectangle (a,b,c,d))))) c= closed_inside_of_rectangle (a,b,c,d)