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 Nat 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 Nat 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 Nat st
( i in dom S & p in Segm (S,i) ) )
assume A1: p in C ; :: thesis: ex i being Nat st
( i in dom S & p in Segm (S,i) )
set X = { i where i is Nat : ( i in dom S & LE S /. i,p,C ) } ;
A2: { i where i is Nat : ( i in dom S & LE S /. i,p,C ) } c= dom S
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { i where i is Nat : ( i in dom S & LE S /. i,p,C ) } or e in dom S )
assume e in { i where i is Nat : ( i in dom S & LE S /. i,p,C ) } ; :: thesis: e in dom S
then ex i being 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 Nat : ( i in dom S & LE S /. i,p,C ) } by A3;
then reconsider X = { i where i is Nat : ( i in dom S & LE S /. i,p,C ) } as non empty finite Subset of NAT by A2, XBOOLE_1:1;
reconsider mX = max X as Nat by TARSKI:1;
take mX ; :: thesis: ( mX in dom S & p in Segm (S,mX) )
A5: max X in X by XXREAL_2:def 8;
hence mX in dom S by A2; :: thesis: p in Segm (S,mX)
A6: 1 <= max X by A2, A5, FINSEQ_3:25;
A7: max X <= len S by A2, A5, FINSEQ_3:25;
A8: ex i being Nat st
( max X = i & i in dom S & LE S /. i,p,C ) by A5;
per cases ( max X < len S or max X = len S ) by A7, XXREAL_0:1;
suppose A9: max X < len S ; :: thesis: p in Segm (S,mX)
A10: 1 <= (max X) + 1 by NAT_1:11;
(max X) + 1 <= len S by A9, NAT_1:13;
then A11: mX + 1 in dom S by A10, FINSEQ_3:25;
A12: S is one-to-one by Def3;
(max X) + 1 >= 1 + 1 by A6, XREAL_1:6;
then (max X) + 1 <> 1 ;
then A13: S /. ((max X) + 1) <> S /. 1 by A3, A11, A12, PARTFUN2:10;
A14: S /. ((max X) + 1) in rng S by A11, PARTFUN2:2;
A15: rng S c= C by Def3;
now :: thesis: not LE S /. ((max X) + 1),p,C
assume LE S /. ((max X) + 1),p,C ; :: thesis: contradiction
then (max X) + 1 in X by A11;
then (max X) + 1 <= max X by XXREAL_2:def 8;
hence contradiction by XREAL_1:29; :: thesis: verum
end;
then LE p,S /. ((max X) + 1),C by A1, A14, A15, JORDAN16:7;
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 A8;
then p in Segment ((S /. (max X)),(S /. ((max X) + 1)),C) by A4, A13, JORDAN7:def 1;
hence p in Segm (S,mX) by A6, A9, Def4; :: thesis: verum
end;
suppose A16: max X = len S ; :: thesis: p in Segm (S,mX)
now :: thesis: ( ( p <> W-min C & LE S /. (len S),p,C ) or ( p = W-min C & S /. (len S) in C ) )
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 A8, A16; :: thesis: verum
end;
case p = W-min C ; :: thesis: S /. (len S) in C
A17: S /. (len S) in rng S by FINSEQ_6:168;
rng S c= C by Def3;
hence S /. (len S) in C by A17; :: 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,mX) by A16, Def4; :: thesis: verum
end;
end;