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

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

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

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

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

assume x in R_Segment (P,p2,p1,q) ; :: thesis: x in L_Segment (P,p1,p2,q)

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

A4: p = x and

A5: LE q,p,P,p2,p1 ;

LE p,q,P,p1,p2 by A1, A5, Th18, JORDAN5B:14;

hence x in L_Segment (P,p1,p2,q) by A4; :: thesis: verum

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

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

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

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R_Segment (P,p2,p1,q) or x in L_Segment (P,p1,p2,q) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L_Segment (P,p1,p2,q) or x in R_Segment (P,p2,p1,q) )

assume x in L_Segment (P,p1,p2,q) ; :: thesis: x in R_Segment (P,p2,p1,q)

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

A2: p = x and

A3: LE p,q,P,p1,p2 ;

LE q,p,P,p2,p1 by A1, A3, Th18;

hence x in R_Segment (P,p2,p1,q) by A2; :: thesis: verum

end;assume x in L_Segment (P,p1,p2,q) ; :: thesis: x in R_Segment (P,p2,p1,q)

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

A2: p = x and

A3: LE p,q,P,p1,p2 ;

LE q,p,P,p2,p1 by A1, A3, Th18;

hence x in R_Segment (P,p2,p1,q) by A2; :: thesis: verum

assume x in R_Segment (P,p2,p1,q) ; :: thesis: x in L_Segment (P,p1,p2,q)

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

A4: p = x and

A5: LE q,p,P,p2,p1 ;

LE p,q,P,p1,p2 by A1, A5, Th18, JORDAN5B:14;

hence x in L_Segment (P,p1,p2,q) by A4; :: thesis: verum