let C be Simple_closed_curve; for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & P c= C holds
ex R being non empty Subset of (TOP-REAL 2) st
( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} )
let P be Subset of (TOP-REAL 2); for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & P c= C holds
ex R being non empty Subset of (TOP-REAL 2) st
( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} )
let p1, p2 be Point of (TOP-REAL 2); ( P is_an_arc_of p1,p2 & P c= C implies ex R being non empty Subset of (TOP-REAL 2) st
( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} ) )
assume that
A1:
P is_an_arc_of p1,p2
and
A2:
P c= C
; ex R being non empty Subset of (TOP-REAL 2) st
( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} )
A3:
p1 <> p2
by A1, JORDAN6:37;
( p1 in P & p2 in P )
by A1, TOPREAL1:1;
then consider P1, P2 being non empty Subset of (TOP-REAL 2) such that
A4:
P1 is_an_arc_of p1,p2
and
A5:
P2 is_an_arc_of p1,p2
and
A6:
C = P1 \/ P2
and
A7:
P1 /\ P2 = {p1,p2}
by A2, A3, TOPREAL2:5;
reconsider P1 = P1, P2 = P2 as non empty Subset of (TOP-REAL 2) ;
A8:
( P1 c= C & P2 c= C )
by A6, XBOOLE_1:7;