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:1;

thus R_Segment (P,p1,p2,p2) c= {p2} :: according to XBOOLE_0:def 10 :: thesis: {p2} c= R_Segment (P,p1,p2,p2)

assume x in {p2} ; :: thesis: x in R_Segment (P,p1,p2,p2)

then A5: 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 A5; :: thesis: verum

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:1;

thus R_Segment (P,p1,p2,p2) c= {p2} :: according to XBOOLE_0:def 10 :: thesis: {p2} c= R_Segment (P,p1,p2,p2)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {p2} or x in R_Segment (P,p1,p2,p2) )
let x be object ; :: 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 and

A4: LE p2,q,P,p1,p2 ;

q in P by A4;

then LE q,p2,P,p1,p2 by A1, JORDAN5C:10;

then q = p2 by A1, A4, JORDAN5C:12;

hence x in {p2} by A3, TARSKI:def 1; :: thesis: verum

end;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 and

A4: LE p2,q,P,p1,p2 ;

q in P by A4;

then LE q,p2,P,p1,p2 by A1, JORDAN5C:10;

then q = p2 by A1, A4, JORDAN5C:12;

hence x in {p2} by A3, TARSKI:def 1; :: thesis: verum

assume x in {p2} ; :: thesis: x in R_Segment (P,p1,p2,p2)

then A5: 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 A5; :: thesis: verum