for P1, P2 being Subset of (TOP-REAL 2)
for a, b, c, d being Real
for f1, f2 being FinSequence of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 = |[a,c]| & p2 = |[b,d]| & f1 = <*|[a,c]|,|[a,d]|,|[b,d]|*> & f2 = <*|[a,c]|,|[b,c]|,|[b,d]|*> & P1 = L~ f1 & P2 = L~ f2 holds
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & not P1 is empty & not P2 is empty & rectangle (a,b,c,d) = P1 \/ P2 & P1 /\ P2 = {p1,p2} )