let P1, P2 be 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} )
let a, b, c, d be 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} )
let f1, f2 be 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} )
let p1, p2 be Point of (TOP-REAL 2); ( 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
; ( 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 A2, EUCLID:52;
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 A2, EUCLID:52;
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; verum