let P be non empty compact Subset of (TOP-REAL 2); for q1, q2, q3 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P & ( not q1 = q2 or not q1 = W-min P ) & ( not q2 = q3 or not q2 = W-min P ) holds
(Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) = {q2}
let q1, q2, q3 be Point of (TOP-REAL 2); ( P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P & ( not q1 = q2 or not q1 = W-min P ) & ( not q2 = q3 or not q2 = W-min P ) implies (Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) = {q2} )
assume that
A1:
P is being_simple_closed_curve
and
A2:
LE q1,q2,P
and
A3:
LE q2,q3,P
and
A4:
( not q1 = q2 or not q1 = W-min P )
and
A5:
( not q2 = q3 or not q2 = W-min P )
; (Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) = {q2}
A6:
Upper_Arc P is_an_arc_of W-min P, E-max P
by A1, JORDAN6:def 8;
thus
(Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) c= {q2}
XBOOLE_0:def 10 {q2} c= (Segment (q1,q2,P)) /\ (Segment (q2,q3,P))proof
let x be
object ;
TARSKI:def 3 ( not x in (Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) or x in {q2} )
assume A7:
x in (Segment (q1,q2,P)) /\ (Segment (q2,q3,P))
;
x in {q2}
then A8:
x in Segment (
q2,
q3,
P)
by XBOOLE_0:def 4;
A9:
x in Segment (
q1,
q2,
P)
by A7, XBOOLE_0:def 4;
now ( ( q3 <> W-min P & x = q2 ) or ( q3 = W-min P & x = q2 ) )per cases
( q3 <> W-min P or q3 = W-min P )
;
case
q3 <> W-min P
;
verumthen
x in { p where p is Point of (TOP-REAL 2) : ( LE q2,p,P & LE p,q3,P ) }
by A8, Def1;
then A10:
ex
p being
Point of
(TOP-REAL 2) st
(
p = x &
LE q2,
p,
P &
LE p,
q3,
P )
;
per cases
( q2 <> W-min P or q2 = W-min P )
;
suppose
q2 <> W-min P
;
x = q2then
x in { p2 where p2 is Point of (TOP-REAL 2) : ( LE q1,p2,P & LE p2,q2,P ) }
by A9, Def1;
then
ex
p2 being
Point of
(TOP-REAL 2) st
(
p2 = x &
LE q1,
p2,
P &
LE p2,
q2,
P )
;
hence
x = q2
by A1, A10, JORDAN6:57;
verum end; end; end; case A12:
q3 = W-min P
;
x = q2then
x in { p1 where p1 is Point of (TOP-REAL 2) : ( LE q2,p1,P or ( q2 in P & p1 = W-min P ) ) }
by A8, Def1;
then consider p1 being
Point of
(TOP-REAL 2) such that A13:
p1 = x
and A14:
(
LE q2,
p1,
P or (
q2 in P &
p1 = W-min P ) )
;
p1 in { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) }
by A5, A9, A12, A13, Def1;
then
ex
p being
Point of
(TOP-REAL 2) st
(
p = p1 &
LE q1,
p,
P &
LE p,
q2,
P )
;
hence
x = q2
by A1, A3, A12, A13, A14, JORDAN6:57;
verum end; end; end;
hence
x in {q2}
by TARSKI:def 1;
verum
end;
let x be object ; TARSKI:def 3 ( not x in {q2} or x in (Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) )
assume
x in {q2}
; x in (Segment (q1,q2,P)) /\ (Segment (q2,q3,P))
then
x = q2
by TARSKI:def 1;
then
( x in Segment (q1,q2,P) & x in Segment (q2,q3,P) )
by A1, A2, A3, Th6;
hence
x in (Segment (q1,q2,P)) /\ (Segment (q2,q3,P))
by XBOOLE_0:def 4; verum