:: JORDAN_A semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: JORDAN_A:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being non empty finite Subset of REAL holds min (A \/ B) = min (min A),(min B)
proof end;

registration
let T be non empty TopSpace;
cluster non empty compact Element of bool the carrier of T;
existence
ex b1 being Subset of T st
( b1 is compact & not b1 is empty )
proof end;
end;

theorem Th2: :: JORDAN_A:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for f being continuous RealMap of T
for A being compact Subset of T holds f .: A is compact
proof end;

theorem Th3: :: JORDAN_A:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being compact Subset of REAL
for B being non empty Subset of REAL st B c= A holds
inf B in A
proof end;

theorem :: JORDAN_A:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for A, B being non empty compact Subset of (TOP-REAL n)
for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]
for g being RealMap of (TOP-REAL n) st ( for p being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . p,q) where q is Point of (TOP-REAL n) : q in B } & g . p = inf G ) ) holds
inf (f .: [:A,B:]) = inf (g .: A)
proof end;

theorem :: JORDAN_A:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for A, B being non empty compact Subset of (TOP-REAL n)
for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]
for g being RealMap of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . p,q) where p is Point of (TOP-REAL n) : p in A } & g . q = inf G ) ) holds
inf (f .: [:A,B:]) = inf (g .: B)
proof end;

theorem Th6: :: JORDAN_A:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for q being Point of (TOP-REAL 2) st q in Lower_Arc C & q <> W-min C holds
LE E-max C,q,C
proof end;

theorem Th7: :: JORDAN_A:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for q being Point of (TOP-REAL 2) st q in Upper_Arc C holds
LE q, E-max C,C
proof end;

definition
let n be Nat;
A1: [:the carrier of (TOP-REAL n),the carrier of (TOP-REAL n):] = the carrier of [:(TOP-REAL n),(TOP-REAL n):] by BORSUK_1:def 5;
func Eucl_dist n -> RealMap of [:(TOP-REAL n),(TOP-REAL n):] means :Def1: :: JORDAN_A:def 1
for p, q being Point of (TOP-REAL n) holds it . p,q = |.(p - q).|;
existence
ex b1 being RealMap of [:(TOP-REAL n),(TOP-REAL n):] st
for p, q being Point of (TOP-REAL n) holds b1 . p,q = |.(p - q).|
proof end;
uniqueness
for b1, b2 being RealMap of [:(TOP-REAL n),(TOP-REAL n):] st ( for p, q being Point of (TOP-REAL n) holds b1 . p,q = |.(p - q).| ) & ( for p, q being Point of (TOP-REAL n) holds b2 . p,q = |.(p - q).| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Eucl_dist JORDAN_A:def 1 :
for n being Nat
for b2 being RealMap of [:(TOP-REAL n),(TOP-REAL n):] holds
( b2 = Eucl_dist n iff for p, q being Point of (TOP-REAL n) holds b2 . p,q = |.(p - q).| );

definition
let T be non empty TopSpace;
let f be RealMap of T;
redefine attr f is continuous means :: JORDAN_A:def 2
for p being Point of T
for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N;
compatibility
( f is continuous iff for p being Point of T
for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N )
proof end;
end;

:: deftheorem defines continuous JORDAN_A:def 2 :
for T being non empty TopSpace
for f being RealMap of T holds
( f is continuous iff for p being Point of T
for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N );

registration
let n be Nat;
cluster Eucl_dist n -> continuous ;
coherence
Eucl_dist n is continuous
proof end;
end;

theorem Th8: :: JORDAN_A:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for A, B being non empty compact Subset of (TOP-REAL n) st A misses B holds
dist_min A,B > 0
proof end;

theorem Th9: :: JORDAN_A:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for p, q being Point of (TOP-REAL 2) st LE p,q,C & LE q, E-max C,C & p <> q holds
Segment p,q,C = Segment (Upper_Arc C),(W-min C),(E-max C),p,q
proof end;

theorem Th10: :: JORDAN_A:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for q being Point of (TOP-REAL 2) st LE E-max C,q,C holds
Segment (E-max C),q,C = Segment (Lower_Arc C),(E-max C),(W-min C),(E-max C),q
proof end;

theorem Th11: :: JORDAN_A:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for q being Point of (TOP-REAL 2) st LE E-max C,q,C holds
Segment q,(W-min C),C = Segment (Lower_Arc C),(E-max C),(W-min C),q,(W-min C)
proof end;

theorem Th12: :: JORDAN_A:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for p, q being Point of (TOP-REAL 2) st LE p,q,C & LE E-max C,p,C holds
Segment p,q,C = Segment (Lower_Arc C),(E-max C),(W-min C),p,q
proof end;

theorem Th13: :: JORDAN_A:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for p, q being Point of (TOP-REAL 2) st LE p, E-max C,C & LE E-max C,q,C holds
Segment p,q,C = (R_Segment (Upper_Arc C),(W-min C),(E-max C),p) \/ (L_Segment (Lower_Arc C),(E-max C),(W-min C),q)
proof end;

theorem Th14: :: JORDAN_A:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for p being Point of (TOP-REAL 2) st LE p, E-max C,C holds
Segment p,(W-min C),C = (R_Segment (Upper_Arc C),(W-min C),(E-max C),p) \/ (L_Segment (Lower_Arc C),(E-max C),(W-min C),(W-min C))
proof end;

theorem Th15: :: JORDAN_A:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for p being Point of (TOP-REAL 2) holds R_Segment (Upper_Arc C),(W-min C),(E-max C),p = Segment (Upper_Arc C),(W-min C),(E-max C),p,(E-max C)
proof end;

theorem Th16: :: JORDAN_A:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for p being Point of (TOP-REAL 2) holds L_Segment (Lower_Arc C),(E-max C),(W-min C),p = Segment (Lower_Arc C),(E-max C),(W-min C),(E-max C),p
proof end;

theorem Th17: :: JORDAN_A:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for p being Point of (TOP-REAL 2) st p in C & p <> W-min C holds
Segment p,(W-min C),C is_an_arc_of p, W-min C
proof end;

theorem Th18: :: JORDAN_A:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for p, q being Point of (TOP-REAL 2) st p <> q & LE p,q,C holds
Segment p,q,C is_an_arc_of p,q
proof end;

theorem Th19: :: JORDAN_A:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve holds C = Segment (W-min C),(W-min C),C
proof end;

theorem Th20: :: JORDAN_A:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for q being Point of (TOP-REAL 2) st q in C holds
Segment q,(W-min C),C is compact
proof end;

theorem Th21: :: JORDAN_A:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for q1, q2 being Point of (TOP-REAL 2) st LE q1,q2,C holds
Segment q1,q2,C is compact
proof end;

definition
let C be Simple_closed_curve;
mode Segmentation of C -> FinSequence of (TOP-REAL 2) means :Def3: :: JORDAN_A:def 3
( it /. 1 = W-min C & it is one-to-one & 8 <= len it & rng it c= C & ( for i being Nat st 1 <= i & i < len it holds
LE it /. i,it /. (i + 1),C ) & ( for i being Nat st 1 <= i & i + 1 < len it holds
(Segment (it /. i),(it /. (i + 1)),C) /\ (Segment (it /. (i + 1)),(it /. (i + 2)),C) = {(it /. (i + 1))} ) & (Segment (it /. (len it)),(it /. 1),C) /\ (Segment (it /. 1),(it /. 2),C) = {(it /. 1)} & (Segment (it /. ((len it) -' 1)),(it /. (len it)),C) /\ (Segment (it /. (len it)),(it /. 1),C) = {(it /. (len it))} & Segment (it /. ((len it) -' 1)),(it /. (len it)),C misses Segment (it /. 1),(it /. 2),C & ( for i, j being Nat st 1 <= i & i < j & j < len it & not i,j are_adjacent1 holds
Segment (it /. i),(it /. (i + 1)),C misses Segment (it /. j),(it /. (j + 1)),C ) & ( for i being Nat st 1 < i & i + 1 < len it holds
Segment (it /. (len it)),(it /. 1),C misses Segment (it /. i),(it /. (i + 1)),C ) );
existence
ex b1 being FinSequence of (TOP-REAL 2) st
( b1 /. 1 = W-min C & b1 is one-to-one & 8 <= len b1 & rng b1 c= C & ( for i being Nat st 1 <= i & i < len b1 holds
LE b1 /. i,b1 /. (i + 1),C ) & ( for i being Nat st 1 <= i & i + 1 < len b1 holds
(Segment (b1 /. i),(b1 /. (i + 1)),C) /\ (Segment (b1 /. (i + 1)),(b1 /. (i + 2)),C) = {(b1 /. (i + 1))} ) & (Segment (b1 /. (len b1)),(b1 /. 1),C) /\ (Segment (b1 /. 1),(b1 /. 2),C) = {(b1 /. 1)} & (Segment (b1 /. ((len b1) -' 1)),(b1 /. (len b1)),C) /\ (Segment (b1 /. (len b1)),(b1 /. 1),C) = {(b1 /. (len b1))} & Segment (b1 /. ((len b1) -' 1)),(b1 /. (len b1)),C misses Segment (b1 /. 1),(b1 /. 2),C & ( for i, j being Nat st 1 <= i & i < j & j < len b1 & not i,j are_adjacent1 holds
Segment (b1 /. i),(b1 /. (i + 1)),C misses Segment (b1 /. j),(b1 /. (j + 1)),C ) & ( for i being Nat st 1 < i & i + 1 < len b1 holds
Segment (b1 /. (len b1)),(b1 /. 1),C misses Segment (b1 /. i),(b1 /. (i + 1)),C ) )
proof end;
end;

:: deftheorem Def3 defines Segmentation JORDAN_A:def 3 :
for C being Simple_closed_curve
for b2 being FinSequence of (TOP-REAL 2) holds
( b2 is Segmentation of C iff ( b2 /. 1 = W-min C & b2 is one-to-one & 8 <= len b2 & rng b2 c= C & ( for i being Nat st 1 <= i & i < len b2 holds
LE b2 /. i,b2 /. (i + 1),C ) & ( for i being Nat st 1 <= i & i + 1 < len b2 holds
(Segment (b2 /. i),(b2 /. (i + 1)),C) /\ (Segment (b2 /. (i + 1)),(b2 /. (i + 2)),C) = {(b2 /. (i + 1))} ) & (Segment (b2 /. (len b2)),(b2 /. 1),C) /\ (Segment (b2 /. 1),(b2 /. 2),C) = {(b2 /. 1)} & (Segment (b2 /. ((len b2) -' 1)),(b2 /. (len b2)),C) /\ (Segment (b2 /. (len b2)),(b2 /. 1),C) = {(b2 /. (len b2))} & Segment (b2 /. ((len b2) -' 1)),(b2 /. (len b2)),C misses Segment (b2 /. 1),(b2 /. 2),C & ( for i, j being Nat st 1 <= i & i < j & j < len b2 & not i,j are_adjacent1 holds
Segment (b2 /. i),(b2 /. (i + 1)),C misses Segment (b2 /. j),(b2 /. (j + 1)),C ) & ( for i being Nat st 1 < i & i + 1 < len b2 holds
Segment (b2 /. (len b2)),(b2 /. 1),C misses Segment (b2 /. i),(b2 /. (i + 1)),C ) ) );

registration
let C be Simple_closed_curve;
cluster -> non trivial Segmentation of C;
coherence
for b1 being Segmentation of C holds not b1 is trivial
proof end;
end;

theorem Th22: :: JORDAN_A:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for S being Segmentation of C
for i being Nat st 1 <= i & i <= len S holds
S /. i in C
proof end;

definition
let C be Simple_closed_curve;
let i be natural number ;
let S be Segmentation of C;
func Segm S,i -> Subset of (TOP-REAL 2) equals :Def4: :: JORDAN_A:def 4
Segment (S /. i),(S /. (i + 1)),C if ( 1 <= i & i < len S )
otherwise Segment (S /. (len S)),(S /. 1),C;
correctness
coherence
( ( 1 <= i & i < len S implies Segment (S /. i),(S /. (i + 1)),C is Subset of (TOP-REAL 2) ) & ( ( not 1 <= i or not i < len S ) implies Segment (S /. (len S)),(S /. 1),C is Subset of (TOP-REAL 2) ) )
;
consistency
for b1 being Subset of (TOP-REAL 2) holds verum
;
;
end;

:: deftheorem Def4 defines Segm JORDAN_A:def 4 :
for C being Simple_closed_curve
for i being natural number
for S being Segmentation of C holds
( ( 1 <= i & i < len S implies Segm S,i = Segment (S /. i),(S /. (i + 1)),C ) & ( ( not 1 <= i or not i < len S ) implies Segm S,i = Segment (S /. (len S)),(S /. 1),C ) );

theorem :: JORDAN_A:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for i being Nat
for S being Segmentation of C st i in dom S holds
Segm S,i c= C
proof end;

registration
let C be Simple_closed_curve;
let S be Segmentation of C;
let i be Nat;
cluster Segm S,i -> non empty compact ;
coherence
( not Segm S,i is empty & Segm S,i is compact )
proof end;
end;

theorem :: JORDAN_A:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
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 )
proof end;

theorem Th25: :: JORDAN_A:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for S being Segmentation of C
for i, j being Nat st 1 <= i & i < j & j < len S & not i,j are_adjacent1 holds
Segm S,i misses Segm S,j
proof end;

theorem Th26: :: JORDAN_A:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for S being Segmentation of C
for j being Nat st 1 < j & j < (len S) -' 1 holds
Segm S,(len S) misses Segm S,j
proof end;

theorem Th27: :: JORDAN_A:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for S being Segmentation of C
for i, j being Nat st 1 <= i & i < j & j < len S & i,j are_adjacent1 holds
(Segm S,i) /\ (Segm S,j) = {(S /. (i + 1))}
proof end;

theorem Th28: :: JORDAN_A:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for S being Segmentation of C
for i, j being Nat st 1 <= i & i < j & j < len S & i,j are_adjacent1 holds
Segm S,i meets Segm S,j
proof end;

theorem Th29: :: JORDAN_A:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for S being Segmentation of C holds (Segm S,(len S)) /\ (Segm S,1) = {(S /. 1)}
proof end;

theorem Th30: :: JORDAN_A:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for S being Segmentation of C holds Segm S,(len S) meets Segm S,1
proof end;

theorem Th31: :: JORDAN_A:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for S being Segmentation of C holds (Segm S,(len S)) /\ (Segm S,((len S) -' 1)) = {(S /. (len S))}
proof end;

theorem Th32: :: JORDAN_A:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for S being Segmentation of C holds Segm S,(len S) meets Segm S,((len S) -' 1)
proof end;

definition
let n be Nat;
let C be Subset of (TOP-REAL n);
func diameter C -> Real means :Def5: :: JORDAN_A:def 5
ex W being Subset of (Euclid n) st
( W = C & it = diameter W );
existence
ex b1 being Real ex W being Subset of (Euclid n) st
( W = C & b1 = diameter W )
proof end;
correctness
uniqueness
for b1, b2 being Real st ex W being Subset of (Euclid n) st
( W = C & b1 = diameter W ) & ex W being Subset of (Euclid n) st
( W = C & b2 = diameter W ) holds
b1 = b2
;
;
end;

:: deftheorem Def5 defines diameter JORDAN_A:def 5 :
for n being Nat
for C being Subset of (TOP-REAL n)
for b3 being Real holds
( b3 = diameter C iff ex W being Subset of (Euclid n) st
( W = C & b3 = diameter W ) );

definition
let C be Simple_closed_curve;
let S be Segmentation of C;
func diameter S -> Real means :Def6: :: JORDAN_A:def 6
ex S1 being non empty finite Subset of REAL st
( S1 = { (diameter (Segm S,i)) where i is Nat : i in dom S } & it = max S1 );
existence
ex b1 being Real ex S1 being non empty finite Subset of REAL st
( S1 = { (diameter (Segm S,i)) where i is Nat : i in dom S } & b1 = max S1 )
proof end;
correctness
uniqueness
for b1, b2 being Real st ex S1 being non empty finite Subset of REAL st
( S1 = { (diameter (Segm S,i)) where i is Nat : i in dom S } & b1 = max S1 ) & ex S1 being non empty finite Subset of REAL st
( S1 = { (diameter (Segm S,i)) where i is Nat : i in dom S } & b2 = max S1 ) holds
b1 = b2
;
;
end;

:: deftheorem Def6 defines diameter JORDAN_A:def 6 :
for C being Simple_closed_curve
for S being Segmentation of C
for b3 being Real holds
( b3 = diameter S iff ex S1 being non empty finite Subset of REAL st
( S1 = { (diameter (Segm S,i)) where i is Nat : i in dom S } & b3 = max S1 ) );

theorem :: JORDAN_A:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for S being Segmentation of C
for i being Nat holds diameter (Segm S,i) <= diameter S
proof end;

theorem Th34: :: JORDAN_A:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for S being Segmentation of C
for e being Real st ( for i being Nat holds diameter (Segm S,i) < e ) holds
diameter S < e
proof end;

theorem :: JORDAN_A:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for e being Real st e > 0 holds
ex S being Segmentation of C st diameter S < e
proof end;

definition
let C be Simple_closed_curve;
let S be Segmentation of C;
func S-Gap S -> Real means :Def7: :: JORDAN_A:def 7
ex S1, S2 being non empty finite Subset of REAL st
( S1 = { (dist_min (Segm S,i),(Segm S,j)) where i, j is Nat : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min (Segm S,(len S)),(Segm S,k)) where k is Nat : ( 1 < k & k < (len S) -' 1 ) } & it = min (min S1),(min S2) );
existence
ex b1 being Real ex S1, S2 being non empty finite Subset of REAL st
( S1 = { (dist_min (Segm S,i),(Segm S,j)) where i, j is Nat : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min (Segm S,(len S)),(Segm S,k)) where k is Nat : ( 1 < k & k < (len S) -' 1 ) } & b1 = min (min S1),(min S2) )
proof end;
correctness
uniqueness
for b1, b2 being Real st ex S1, S2 being non empty finite Subset of REAL st
( S1 = { (dist_min (Segm S,i),(Segm S,j)) where i, j is Nat : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min (Segm S,(len S)),(Segm S,k)) where k is Nat : ( 1 < k & k < (len S) -' 1 ) } & b1 = min (min S1),(min S2) ) & ex S1, S2 being non empty finite Subset of REAL st
( S1 = { (dist_min (Segm S,i),(Segm S,j)) where i, j is Nat : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min (Segm S,(len S)),(Segm S,k)) where k is Nat : ( 1 < k & k < (len S) -' 1 ) } & b2 = min (min S1),(min S2) ) holds
b1 = b2
;
;
end;

:: deftheorem Def7 defines S-Gap JORDAN_A:def 7 :
for C being Simple_closed_curve
for S being Segmentation of C
for b3 being Real holds
( b3 = S-Gap S iff ex S1, S2 being non empty finite Subset of REAL st
( S1 = { (dist_min (Segm S,i),(Segm S,j)) where i, j is Nat : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min (Segm S,(len S)),(Segm S,k)) where k is Nat : ( 1 < k & k < (len S) -' 1 ) } & b3 = min (min S1),(min S2) ) );

theorem Th36: :: JORDAN_A:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for S being Segmentation of C ex F being non empty finite Subset of REAL st
( F = { (dist_min (Segm S,i),(Segm S,j)) where i, j is Nat : ( 1 <= i & i < j & j <= len S & Segm S,i misses Segm S,j ) } & S-Gap S = min F )
proof end;

theorem :: JORDAN_A:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for S being Segmentation of C holds S-Gap S > 0
proof end;