let P be Subset of (TOP-REAL 2); for p1, p2, p being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & p in P holds
Segment (P,p1,p2,p,p) = {p}
let p1, p2, p be Point of (TOP-REAL 2); ( P is_an_arc_of p1,p2 & p in P implies Segment (P,p1,p2,p,p) = {p} )
assume that
A1:
P is_an_arc_of p1,p2
and
A2:
p in P
; Segment (P,p1,p2,p,p) = {p}
A3:
Segment (P,p1,p2,p,p) = { q where q is Point of (TOP-REAL 2) : ( LE p,q,P,p1,p2 & LE q,p,P,p1,p2 ) }
by JORDAN6:26;
A4:
{p} c= Segment (P,p1,p2,p,p)
proof
let x be
object ;
TARSKI:def 3 ( not x in {p} or x in Segment (P,p1,p2,p,p) )
assume
x in {p}
;
x in Segment (P,p1,p2,p,p)
then A5:
x = p
by TARSKI:def 1;
LE p,
p,
P,
p1,
p2
by A2, JORDAN5C:9;
hence
x in Segment (
P,
p1,
p2,
p,
p)
by A3, A5;
verum
end;
Segment (P,p1,p2,p,p) c= {p}
proof
let x be
object ;
TARSKI:def 3 ( not x in Segment (P,p1,p2,p,p) or x in {p} )
assume
x in Segment (
P,
p1,
p2,
p,
p)
;
x in {p}
then consider q being
Point of
(TOP-REAL 2) such that A6:
x = q
and A7:
(
LE p,
q,
P,
p1,
p2 &
LE q,
p,
P,
p1,
p2 )
by A3;
p = q
by A1, A7, JORDAN5C:12;
hence
x in {p}
by A6, TARSKI:def 1;
verum
end;
hence
Segment (P,p1,p2,p,p) = {p}
by A4, XBOOLE_0:def 10; verum