let C be Simple_closed_curve; :: thesis: for A1, A2 being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st A1 c= C & A2 c= C & A1 <> A2 & A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 holds
for A being Subset of (TOP-REAL 2) st A is_an_arc_of p1,p2 & A c= C & not A = A1 holds
A = A2
let A1, A2 be Subset of (TOP-REAL 2); :: thesis: for p1, p2 being Point of (TOP-REAL 2) st A1 c= C & A2 c= C & A1 <> A2 & A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 holds
for A being Subset of (TOP-REAL 2) st A is_an_arc_of p1,p2 & A c= C & not A = A1 holds
A = A2
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( A1 c= C & A2 c= C & A1 <> A2 & A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 implies for A being Subset of (TOP-REAL 2) st A is_an_arc_of p1,p2 & A c= C & not A = A1 holds
A = A2 )
assume that
A1:
A1 c= C
and
A2:
A2 c= C
and
A3:
A1 <> A2
and
A4:
A1 is_an_arc_of p1,p2
and
A5:
A2 is_an_arc_of p1,p2
; :: thesis: for A being Subset of (TOP-REAL 2) st A is_an_arc_of p1,p2 & A c= C & not A = A1 holds
A = A2
let A be Subset of (TOP-REAL 2); :: thesis: ( A is_an_arc_of p1,p2 & A c= C & not A = A1 implies A = A2 )
assume that
A6:
A is_an_arc_of p1,p2
and
A7:
A c= C
; :: thesis: ( A = A1 or A = A2 )
A8:
A1 \/ A2 = C
by A1, A2, A3, A4, A5, Th15;
A1 /\ A2 = {p1,p2}
by A1, A2, A3, A4, A5, Th15;
hence
( A = A1 or A = A2 )
by A4, A5, A6, A7, A8, Th14; :: thesis: verum