let C be Simple_closed_curve; :: thesis: for S being Segmentation of C
for p being Point of (TOP-REAL 2) st p in C holds
ex i being natural number st
( i in dom S & p in Segm S,i )
let S be Segmentation of C; :: thesis: for p being Point of (TOP-REAL 2) st p in C holds
ex i being natural number st
( i in dom S & p in Segm S,i )
let p be Point of (TOP-REAL 2); :: thesis: ( p in C implies ex i being natural number st
( i in dom S & p in Segm S,i ) )
assume A1: p in C ; :: thesis: ex i being natural number st
( i in dom S & p in Segm S,i )
set X = { i where i is Element of NAT : ( i in dom S & LE S /. i,p,C ) } ;
A2: { i where i is Element of NAT : ( i in dom S & LE S /. i,p,C ) } c= dom S

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { i where i is Element of NAT : ( i in dom S & LE S /. i,p,C ) } or e in dom S )
assume e in { i where i is Element of NAT : ( i in dom S & LE S /. i,p,C ) } ; :: thesis: e in dom S
then ex i being Element of NAT st
( e = i & i in dom S & LE S /. i,p,C ) ;
hence e in dom S ; :: thesis: verum

end;

A3: 1 in dom S by FINSEQ_5:6;
A4: W-min C = S /. 1 by Def3;
then LE S /. 1,p,C by A1, JORDAN7:3;
then 1 in { i where i is Element of NAT : ( i in dom S & LE S /. i,p,C ) } by A3;
then reconsider X = { i where i is Element of NAT : ( i in dom S & LE S /. i,p,C ) } as non empty finite Subset of NAT by A2, XBOOLE_1:1;
take max X ; :: thesis: ( max X in dom S & p in Segm S,(max X) )
A5: max X in X by XXREAL_2:def 8;
hence max X in dom S by A2; :: thesis: p in Segm S,(max X)
A6: ( 1 <= max X & max X <= len S ) by A2, A5, FINSEQ_3:27;
A7: ex i being Element of NAT st
( max X = i & i in dom S & LE S /. i,p,C ) by A5;
reconsider mX = max X as Element of NAT by ORDINAL1:def 13;

per cases ( max X < len S or max X = len S ) by A6, XXREAL_0:1;

suppose A8: max X < len S ; :: thesis: p in Segm S,(max X)

then ( 1 <= (max X) + 1 & (max X) + 1 <= len S ) by NAT_1:11, NAT_1:13;
then A9: mX + 1 in dom S by FINSEQ_3:27;
A10: S is one-to-one by Def3;
(max X) + 1 >= 1 + 1 by A6, XREAL_1:8;
then (max X) + 1 <> 1 ;
then A11: S /. ((max X) + 1) <> S /. 1 by A3, A9, A10, PARTFUN2:17;
A12: S /. ((max X) + 1) in rng S by A9, PARTFUN2:4;
A13: rng S c= C by Def3;

now

assume LE S /. ((max X) + 1),p,C ; :: thesis: contradiction
then (max X) + 1 in X by A9;
then (max X) + 1 <= max X by XXREAL_2:def 8;
hence contradiction by XREAL_1:31; :: thesis: verum

end;

then LE p,S /. ((max X) + 1),C by A1, A12, A13, JORDAN16:11;
then p in { p1 where p1 is Point of (TOP-REAL 2) : ( LE S /. (max X),p1,C & LE p1,S /. ((max X) + 1),C ) } by A7;
then p in Segment (S /. (max X)),(S /. ((max X) + 1)),C by A4, A11, JORDAN7:def 1;
hence p in Segm S,(max X) by A6, A8, Def4; :: thesis: verum

end;

suppose A14: max X = len S ; :: thesis: p in Segm S,(max X)

now

per cases ( p <> W-min C or p = W-min C ) ;

case p <> W-min C ; :: thesis: LE S /. (len S),p,C

thus LE S /. (len S),p,C by A7, A14; :: thesis: verum

end;

case p = W-min C ; :: thesis: S /. (len S) in C

A15: S /. (len S) in rng S by REVROT_1:3;
rng S c= C by Def3;
hence S /. (len S) in C by A15; :: thesis: verum

end;

end;

end;

then p in { p1 where p1 is Point of (TOP-REAL 2) : ( LE S /. (len S),p1,C or ( S /. (len S) in C & p1 = W-min C ) ) } ;
then p in Segment (S /. (len S)),(S /. 1),C by A4, JORDAN7:def 1;
hence p in Segm S,(max X) by A14, Def4; :: thesis: verum

end;

end;