let P be Subset of (TOP-REAL 2); :: thesis: 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); :: thesis: ( P is_an_arc_of p1,p2 & p in P implies Segment P,p1,p2,p,p = {p} )
assume A1:
( P is_an_arc_of p1,p2 & p in P )
; :: thesis: Segment P,p1,p2,p,p = {p}
A2:
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:29;
A3:
Segment P,p1,p2,p,p c= {p}
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in Segment P,p1,p2,p,p or x in {p} )
assume
x in Segment P,
p1,
p2,
p,
p
;
:: thesis: x in {p}
then consider q being
Point of
(TOP-REAL 2) such that A4:
(
x = q &
LE p,
q,
P,
p1,
p2 &
LE q,
p,
P,
p1,
p2 )
by A2;
p = q
by A1, A4, JORDAN5C:12;
hence
x in {p}
by A4, TARSKI:def 1;
:: thesis: verum
end;
{p} c= Segment P,p1,p2,p,p
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in {p} or x in Segment P,p1,p2,p,p )
assume
x in {p}
;
:: thesis: x in Segment P,p1,p2,p,p
then A5:
x = p
by TARSKI:def 1;
LE p,
p,
P,
p1,
p2
by A1, JORDAN5C:9;
hence
x in Segment P,
p1,
p2,
p,
p
by A2, A5;
:: thesis: verum
end;
hence
Segment P,p1,p2,p,p = {p}
by A3, XBOOLE_0:def 10; :: thesis: verum