let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
R_Segment P,p1,p2,p2 = {p2}
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 implies R_Segment P,p1,p2,p2 = {p2} )
assume A1:
P is_an_arc_of p1,p2
; :: thesis: R_Segment P,p1,p2,p2 = {p2}
then A2:
p2 in P
by TOPREAL1:4;
thus
R_Segment P,p1,p2,p2 c= {p2}
:: according to XBOOLE_0:def 10 :: thesis: {p2} c= R_Segment P,p1,p2,p2proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in R_Segment P,p1,p2,p2 or x in {p2} )
assume
x in R_Segment P,
p1,
p2,
p2
;
:: thesis: x in {p2}
then consider q being
Point of
(TOP-REAL 2) such that A3:
(
q = x &
LE p2,
q,
P,
p1,
p2 )
;
q in P
by A3, JORDAN5C:def 3;
then
(
LE p1,
q,
P,
p1,
p2 &
LE q,
p2,
P,
p1,
p2 )
by A1, JORDAN5C:10;
then
q = p2
by A1, A3, JORDAN5C:12;
hence
x in {p2}
by A3, TARSKI:def 1;
:: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {p2} or x in R_Segment P,p1,p2,p2 )
assume
x in {p2}
; :: thesis: x in R_Segment P,p1,p2,p2
then A4:
x = p2
by TARSKI:def 1;
LE p2,p2,P,p1,p2
by A2, JORDAN5C:9;
hence
x in R_Segment P,p1,p2,p2
by A4; :: thesis: verum