let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q1 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

R_Segment (P,p1,p2,q1) = L_Segment (P,p2,p1,q1)

let p1, p2, q1 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 implies R_Segment (P,p1,p2,q1) = L_Segment (P,p2,p1,q1) )

assume A1: P is_an_arc_of p1,p2 ; :: thesis: R_Segment (P,p1,p2,q1) = L_Segment (P,p2,p1,q1)

A2: { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } c= { q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 }

R_Segment (P,p1,p2,q1) = L_Segment (P,p2,p1,q1)

let p1, p2, q1 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 implies R_Segment (P,p1,p2,q1) = L_Segment (P,p2,p1,q1) )

assume A1: P is_an_arc_of p1,p2 ; :: thesis: R_Segment (P,p1,p2,q1) = L_Segment (P,p2,p1,q1)

A2: { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } c= { q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 }

proof

{ q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 } c= { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 }
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } or x in { q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 } )

assume x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } ; :: thesis: x in { q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 }

then consider q being Point of (TOP-REAL 2) such that

A3: q = x and

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

LE q,q1,P,p2,p1 by A1, A4, Th18;

hence x in { q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 } by A3; :: thesis: verum

end;assume x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } ; :: thesis: x in { q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 }

then consider q being Point of (TOP-REAL 2) such that

A3: q = x and

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

LE q,q1,P,p2,p1 by A1, A4, Th18;

hence x in { q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 } by A3; :: thesis: verum

proof

hence
R_Segment (P,p1,p2,q1) = L_Segment (P,p2,p1,q1)
by A2; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 } or x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } )

assume x in { q where q is Point of (TOP-REAL 2) : LE q,q1,P,p2,p1 } ; :: thesis: x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 }

then consider q being Point of (TOP-REAL 2) such that

A5: q = x and

A6: LE q,q1,P,p2,p1 ;

LE q1,q,P,p1,p2 by A1, A6, Th18, JORDAN5B:14;

hence x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } by A5; :: thesis: verum

end;assume x in { q where q is Point of (TOP-REAL 2) : LE q,q1,P,p2,p1 } ; :: thesis: x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 }

then consider q being Point of (TOP-REAL 2) such that

A5: q = x and

A6: LE q,q1,P,p2,p1 ;

LE q1,q,P,p1,p2 by A1, A6, Th18, JORDAN5B:14;

hence x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } by A5; :: thesis: verum