let P1, P2 be Subset of (); :: thesis: for a, b, c, d being Real
for f1, f2 being FinSequence of ()
for p1, p2 being Point of () 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} )

let a, b, c, d be Real; :: thesis: for f1, f2 being FinSequence of ()
for p1, p2 being Point of () 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} )

let f1, f2 be FinSequence of (); :: thesis: for p1, p2 being Point of () 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} )

let p1, p2 be Point of (); :: thesis: ( 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 implies ( 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} ) )
assume that
A1: a < b and
A2: c < d and
A3: p1 = |[a,c]| and
A4: p2 = |[b,d]| and
A5: f1 = <*|[a,c]|,|[a,d]|,|[b,d]|*> and
A6: f2 = <*|[a,c]|,|[b,c]|,|[b,d]|*> and
A7: P1 = L~ f1 and
A8: P2 = L~ f2 ; :: thesis: ( 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} )
|[a,c]| `2 = c by EUCLID:52;
then A9: ( |[a,c]| <> |[a,d]| or |[a,d]| <> |[b,d]| ) by ;
A10: P1 = (LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|)) by A1, A2, A5, A6, A7, Th48;
A11: (LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,d]|,|[b,d]|)) = {|[a,d]|} by A1, A2, Th34;
|[b,c]| `2 = c by EUCLID:52;
then A12: ( |[a,c]| <> |[b,c]| or |[b,c]| <> |[b,d]| ) by ;
A13: P2 = (LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|)) by A1, A2, A5, A6, A8, Th48;
(LSeg (|[a,c]|,|[b,c]|)) /\ (LSeg (|[b,c]|,|[b,d]|)) = {|[b,c]|} by A1, A2, Th32;
hence ( 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} ) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, Th48, TOPREAL1:12; :: thesis: verum