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

theorem Th1: :: JORDAN2C:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being Real st r <= 0 holds
abs r = - r
proof end;

theorem Th2: :: JORDAN2C:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat st n <= m & m <= n + 2 & not m = n & not m = n + 1 holds
m = n + 2
proof end;

theorem Th3: :: JORDAN2C:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat st n <= m & m <= n + 3 & not m = n & not m = n + 1 & not m = n + 2 holds
m = n + 3
proof end;

theorem Th4: :: JORDAN2C:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat st n <= m & m <= n + 4 & not m = n & not m = n + 1 & not m = n + 2 & not m = n + 3 holds
m = n + 4
proof end;

Lm1: for a, b being real number st a >= 0 & b >= 0 holds
a + b >= 0
by XREAL_1:35;

Lm2: for a, b being real number st a > 0 & b >= 0 holds
a + b > 0
by XREAL_1:36;

theorem :: JORDAN2C:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: JORDAN2C:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th7: :: JORDAN2C:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set
for f being FinSequence st rng f = {x,y} & len f = 2 & not ( f . 1 = x & f . 2 = y ) holds
( f . 1 = y & f . 2 = x )
proof end;

theorem Th8: :: JORDAN2C:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, s being Real
for f being increasing FinSequence of REAL st rng f = {r,s} & len f = 2 & r <= s holds
( f . 1 = r & f . 2 = s )
proof end;

theorem Th9: :: JORDAN2C:9  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 p1, p2, p3 being Point of (TOP-REAL n) holds (p1 + p2) - p3 = (p1 - p3) + p2
proof end;

theorem :: JORDAN2C:10  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 q being Point of (TOP-REAL n) holds abs |.q.| = |.q.|
proof end;

theorem Th11: :: JORDAN2C:11  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 q1, q2 being Point of (TOP-REAL n) holds abs (|.q1.| - |.q2.|) <= |.(q1 - q2).|
proof end;

theorem Th12: :: JORDAN2C:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being Real holds |.|[r]|.| = abs r
proof end;

theorem Th13: :: JORDAN2C:13  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 q being Point of (TOP-REAL n) holds
( q - (0.REAL n) = q & (0.REAL n) - q = - q )
proof end;

theorem Th14: :: JORDAN2C:14  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 P being Subset of (TOP-REAL n) st P is convex holds
P is connected
proof end;

theorem Th15: :: JORDAN2C:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty TopSpace
for P, A being Subset of G
for Q being Subset of (G | A) st P = Q & P is connected holds
Q is connected
proof end;

definition
let n be Nat;
let A be Subset of (TOP-REAL n);
canceled;
attr A is Bounded means :Def2: :: JORDAN2C:def 2
A is bounded Subset of (Euclid n);
correctness
;
end;

:: deftheorem JORDAN2C:def 1 :
canceled;

:: deftheorem Def2 defines Bounded JORDAN2C:def 2 :
for n being Nat
for A being Subset of (TOP-REAL n) holds
( A is Bounded iff A is bounded Subset of (Euclid n) );

theorem Th16: :: JORDAN2C:16  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 Subset of (TOP-REAL n) st B is Bounded & A c= B holds
A is Bounded
proof end;

definition
let n be Nat;
let A, B be Subset of (TOP-REAL n);
pred B is_inside_component_of A means :Def3: :: JORDAN2C:def 3
( B is_a_component_of A ` & B is Bounded );
end;

:: deftheorem Def3 defines is_inside_component_of JORDAN2C:def 3 :
for n being Nat
for A, B being Subset of (TOP-REAL n) holds
( B is_inside_component_of A iff ( B is_a_component_of A ` & B is Bounded ) );

registration
let M be non empty MetrStruct ;
cluster bounded Element of bool the carrier of M;
existence
ex b1 being Subset of M st b1 is bounded
proof end;
end;

theorem Th17: :: JORDAN2C:17  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 Subset of (TOP-REAL n) holds
( B is_inside_component_of A iff ex C being Subset of ((TOP-REAL n) | (A ` )) st
( C = B & C is_a_component_of (TOP-REAL n) | (A ` ) & C is bounded Subset of (Euclid n) ) )
proof end;

definition
let n be Nat;
let A, B be Subset of (TOP-REAL n);
pred B is_outside_component_of A means :Def4: :: JORDAN2C:def 4
( B is_a_component_of A ` & not B is Bounded );
end;

:: deftheorem Def4 defines is_outside_component_of JORDAN2C:def 4 :
for n being Nat
for A, B being Subset of (TOP-REAL n) holds
( B is_outside_component_of A iff ( B is_a_component_of A ` & not B is Bounded ) );

theorem Th18: :: JORDAN2C:18  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 Subset of (TOP-REAL n) holds
( B is_outside_component_of A iff ex C being Subset of ((TOP-REAL n) | (A ` )) st
( C = B & C is_a_component_of (TOP-REAL n) | (A ` ) & C is not bounded Subset of (Euclid n) ) )
proof end;

theorem :: JORDAN2C:19  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 Subset of (TOP-REAL n) st B is_inside_component_of A holds
B c= A `
proof end;

theorem :: JORDAN2C:20  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 Subset of (TOP-REAL n) st B is_outside_component_of A holds
B c= A `
proof end;

definition
let n be Nat;
let A be Subset of (TOP-REAL n);
func BDD A -> Subset of (TOP-REAL n) equals :: JORDAN2C:def 5
union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } ;
correctness
coherence
union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } is Subset of (TOP-REAL n)
;
proof end;
end;

:: deftheorem defines BDD JORDAN2C:def 5 :
for n being Nat
for A being Subset of (TOP-REAL n) holds BDD A = union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } ;

definition
let n be Nat;
let A be Subset of (TOP-REAL n);
func UBD A -> Subset of (TOP-REAL n) equals :: JORDAN2C:def 6
union { B where B is Subset of (TOP-REAL n) : B is_outside_component_of A } ;
correctness
coherence
union { B where B is Subset of (TOP-REAL n) : B is_outside_component_of A } is Subset of (TOP-REAL n)
;
proof end;
end;

:: deftheorem defines UBD JORDAN2C:def 6 :
for n being Nat
for A being Subset of (TOP-REAL n) holds UBD A = union { B where B is Subset of (TOP-REAL n) : B is_outside_component_of A } ;

theorem Th21: :: JORDAN2C:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds [#] (TOP-REAL n) is convex
proof end;

theorem Th22: :: JORDAN2C:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds [#] (TOP-REAL n) is connected
proof end;

registration
let n be Nat;
cluster [#] (TOP-REAL n) -> connected ;
coherence
[#] (TOP-REAL n) is connected
by Th22;
end;

theorem Th23: :: JORDAN2C:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds [#] (TOP-REAL n) is_a_component_of TOP-REAL n
proof end;

theorem Th24: :: JORDAN2C:24  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 being Subset of (TOP-REAL n) holds BDD A is a_union_of_components of (TOP-REAL n) | (A ` )
proof end;

theorem Th25: :: JORDAN2C:25  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 being Subset of (TOP-REAL n) holds UBD A is a_union_of_components of (TOP-REAL n) | (A ` )
proof end;

theorem Th26: :: JORDAN2C:26  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 Subset of (TOP-REAL n) st B is_inside_component_of A holds
B c= BDD A
proof end;

theorem Th27: :: JORDAN2C:27  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 Subset of (TOP-REAL n) st B is_outside_component_of A holds
B c= UBD A
proof end;

theorem Th28: :: JORDAN2C:28  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 being Subset of (TOP-REAL n) holds BDD A misses UBD A
proof end;

theorem Th29: :: JORDAN2C:29  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 being Subset of (TOP-REAL n) holds BDD A c= A `
proof end;

theorem Th30: :: JORDAN2C:30  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 being Subset of (TOP-REAL n) holds UBD A c= A `
proof end;

theorem Th31: :: JORDAN2C:31  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 being Subset of (TOP-REAL n) holds (BDD A) \/ (UBD A) = A `
proof end;

theorem Th32: :: JORDAN2C:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty TopSpace
for w1, w2, w3 being Point of G
for h1, h2 being Function of I[01] ,G st h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 holds
ex h3 being Function of I[01] ,G st
( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) )
proof end;

theorem Th33: :: JORDAN2C:33  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 P being Subset of (TOP-REAL n) st P = REAL n holds
P is connected
proof end;

definition
let n be Nat;
func 1* n -> FinSequence of REAL equals :: JORDAN2C:def 7
n |-> 1;
coherence
n |-> 1 is FinSequence of REAL
by FINSEQ_2:77;
end;

:: deftheorem defines 1* JORDAN2C:def 7 :
for n being Nat holds 1* n = n |-> 1;

definition
let n be Nat;
:: original: 1*
redefine func 1* n -> Element of REAL n;
coherence
1* n is Element of REAL n
proof end;
end;

definition
let n be Nat;
func 1.REAL n -> Point of (TOP-REAL n) equals :: JORDAN2C:def 8
1* n;
coherence
1* n is Point of (TOP-REAL n)
by EUCLID:25;
end;

:: deftheorem defines 1.REAL JORDAN2C:def 8 :
for n being Nat holds 1.REAL n = 1* n;

theorem :: JORDAN2C:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds abs (1* n) = n |-> 1
proof end;

theorem Th35: :: JORDAN2C:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds |.(1* n).| = sqrt n
proof end;

theorem Th36: :: JORDAN2C:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
1.REAL 1 = <*1*> by FINSEQ_2:73;

theorem Th37: :: JORDAN2C:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds |.(1.REAL n).| = sqrt n
proof end;

theorem Th38: :: JORDAN2C:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat st 1 <= n holds
1 <= |.(1.REAL n).|
proof end;

theorem Th39: :: JORDAN2C:39  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 W being Subset of (Euclid n) st n >= 1 & W = REAL n holds
not W is bounded
proof end;

theorem Th40: :: JORDAN2C:40  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 being Subset of (TOP-REAL n) holds
( A is Bounded iff ex r being Real st
for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r )
proof end;

theorem Th41: :: JORDAN2C:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat st n >= 1 holds
not [#] (TOP-REAL n) is Bounded
proof end;

theorem Th42: :: JORDAN2C:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat st n >= 1 holds
UBD ({} (TOP-REAL n)) = REAL n
proof end;

theorem Th43: :: JORDAN2C:43  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 w1, w2, w3 being Point of (TOP-REAL n)
for P being non empty Subset of (TOP-REAL n)
for h1, h2 being Function of I[01] ,((TOP-REAL n) | P) st h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 holds
ex h3 being Function of I[01] ,((TOP-REAL n) | P) st
( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 )
proof end;

theorem Th44: :: JORDAN2C:44  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 P being Subset of (TOP-REAL n)
for w1, w2, w3 being Point of (TOP-REAL n) st w1 in P & w2 in P & w3 in P & LSeg w1,w2 c= P & LSeg w2,w3 c= P holds
ex h being Function of I[01] ,((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w3 = h . 1 )
proof end;

theorem Th45: :: JORDAN2C:45  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 P being Subset of (TOP-REAL n)
for w1, w2, w3, w4 being Point of (TOP-REAL n) st w1 in P & w2 in P & w3 in P & w4 in P & LSeg w1,w2 c= P & LSeg w2,w3 c= P & LSeg w3,w4 c= P holds
ex h being Function of I[01] ,((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w4 = h . 1 )
proof end;

theorem Th46: :: JORDAN2C:46  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 P being Subset of (TOP-REAL n)
for w1, w2, w3, w4, w5, w6, w7 being Point of (TOP-REAL n) st w1 in P & w2 in P & w3 in P & w4 in P & w5 in P & w6 in P & w7 in P & LSeg w1,w2 c= P & LSeg w2,w3 c= P & LSeg w3,w4 c= P & LSeg w4,w5 c= P & LSeg w5,w6 c= P & LSeg w6,w7 c= P holds
ex h being Function of I[01] ,((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w7 = h . 1 )
proof end;

theorem Th47: :: JORDAN2C:47  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 w1, w2 being Point of (TOP-REAL n) st ( for r being Real holds
( not w1 = r * w2 & not w2 = r * w1 ) ) holds
not 0.REAL n in LSeg w1,w2
proof end;

theorem Th48: :: JORDAN2C:48  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 w1, w2 being Point of (TOP-REAL n)
for P being Subset of (TopSpaceMetr (Euclid n)) st P = LSeg w1,w2 & not 0.REAL n in LSeg w1,w2 holds
ex w0 being Point of (TOP-REAL n) st
( w0 in LSeg w1,w2 & |.w0.| > 0 & |.w0.| = (dist_min P) . (0.REAL n) )
proof end;

theorem Th49: :: JORDAN2C:49  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 being Real
for Q being Subset of (TOP-REAL n)
for w1, w4 being Point of (TOP-REAL n) st Q = { q where q is Point of (TOP-REAL n) : |.q.| > a } & w1 in Q & w4 in Q & ( for r being Real holds
( not w1 = r * w4 & not w4 = r * w1 ) ) holds
ex w2, w3 being Point of (TOP-REAL n) st
( w2 in Q & w3 in Q & LSeg w1,w2 c= Q & LSeg w2,w3 c= Q & LSeg w3,w4 c= Q )
proof end;

theorem Th50: :: JORDAN2C:50  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 being Real
for Q being Subset of (TOP-REAL n)
for w1, w4 being Point of (TOP-REAL n) st Q = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } & w1 in Q & w4 in Q & ( for r being Real holds
( not w1 = r * w4 & not w4 = r * w1 ) ) holds
ex w2, w3 being Point of (TOP-REAL n) st
( w2 in Q & w3 in Q & LSeg w1,w2 c= Q & LSeg w2,w3 c= Q & LSeg w3,w4 c= Q )
proof end;

theorem :: JORDAN2C:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th52: :: JORDAN2C:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL holds
( f is Element of REAL (len f) & f is Point of (TOP-REAL (len f)) )
proof end;

theorem Th53: :: JORDAN2C:53  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 x being Element of REAL n
for f, g being FinSequence of REAL
for r being Real st f = x & g = r * x holds
( len f = len g & ( for i being Nat st 1 <= i & i <= len f holds
g /. i = r * (f /. i) ) )
proof end;

theorem Th54: :: JORDAN2C:54  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 x being Element of REAL n
for f being FinSequence st x <> 0* n & x = f holds
ex i being Nat st
( 1 <= i & i <= n & f . i <> 0 )
proof end;

theorem Th55: :: JORDAN2C:55  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 x being Element of REAL n st n >= 2 & x <> 0* n holds
ex y being Element of REAL n st
for r being Real holds
( not y = r * x & not x = r * y )
proof end;

theorem Th56: :: JORDAN2C:56  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 being Real
for Q being Subset of (TOP-REAL n)
for w1, w7 being Point of (TOP-REAL n) st n >= 2 & Q = { q where q is Point of (TOP-REAL n) : |.q.| > a } & w1 in Q & w7 in Q & ex r being Real st
( w1 = r * w7 or w7 = r * w1 ) holds
ex w2, w3, w4, w5, w6 being Point of (TOP-REAL n) st
( w2 in Q & w3 in Q & w4 in Q & w5 in Q & w6 in Q & LSeg w1,w2 c= Q & LSeg w2,w3 c= Q & LSeg w3,w4 c= Q & LSeg w4,w5 c= Q & LSeg w5,w6 c= Q & LSeg w6,w7 c= Q )
proof end;

theorem Th57: :: JORDAN2C:57  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 being Real
for Q being Subset of (TOP-REAL n)
for w1, w7 being Point of (TOP-REAL n) st n >= 2 & Q = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } & w1 in Q & w7 in Q & ex r being Real st
( w1 = r * w7 or w7 = r * w1 ) holds
ex w2, w3, w4, w5, w6 being Point of (TOP-REAL n) st
( w2 in Q & w3 in Q & w4 in Q & w5 in Q & w6 in Q & LSeg w1,w2 c= Q & LSeg w2,w3 c= Q & LSeg w3,w4 c= Q & LSeg w4,w5 c= Q & LSeg w5,w6 c= Q & LSeg w6,w7 c= Q )
proof end;

theorem Th58: :: JORDAN2C:58  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 being Real st n >= 1 holds
{ q where q is Point of (TOP-REAL n) : |.q.| > a } <> {}
proof end;

theorem Th59: :: JORDAN2C:59  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 being Real
for P being Subset of (TOP-REAL n) st n >= 2 & P = { q where q is Point of (TOP-REAL n) : |.q.| > a } holds
P is connected
proof end;

theorem Th60: :: JORDAN2C:60  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 being Real st n >= 1 holds
(REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } <> {}
proof end;

theorem Th61: :: JORDAN2C:61  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 being Real
for P being Subset of (TOP-REAL n) st n >= 2 & P = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } holds
P is connected
proof end;

theorem Th62: :: JORDAN2C:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Real
for n being Nat
for P being Subset of (TOP-REAL n) st n >= 1 & P = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } holds
not P is Bounded
proof end;

theorem Th63: :: JORDAN2C:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Real
for P being Subset of (TOP-REAL 1) st P = { q where q is Point of (TOP-REAL 1) : ex r being Real st
( q = <*r*> & r > a )
}
holds
P is convex
proof end;

theorem Th64: :: JORDAN2C:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Real
for P being Subset of (TOP-REAL 1) st P = { q where q is Point of (TOP-REAL 1) : ex r being Real st
( q = <*r*> & r < - a )
}
holds
P is convex
proof end;

theorem Th65: :: JORDAN2C:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Real
for P being Subset of (TOP-REAL 1) st P = { q where q is Point of (TOP-REAL 1) : ex r being Real st
( q = <*r*> & r > a )
}
holds
P is connected
proof end;

theorem Th66: :: JORDAN2C:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Real
for P being Subset of (TOP-REAL 1) st P = { q where q is Point of (TOP-REAL 1) : ex r being Real st
( q = <*r*> & r < - a )
}
holds
P is connected
proof end;

theorem Th67: :: JORDAN2C:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Subset of (Euclid 1)
for a being Real
for P being Subset of (TOP-REAL 1) st W = { q where q is Point of (TOP-REAL 1) : ex r being Real st
( q = <*r*> & r > a )
}
& P = W holds
( P is connected & not W is bounded )
proof end;

theorem Th68: :: JORDAN2C:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Subset of (Euclid 1)
for a being Real
for P being Subset of (TOP-REAL 1) st W = { q where q is Point of (TOP-REAL 1) : ex r being Real st
( q = <*r*> & r < - a )
}
& P = W holds
( P is connected & not W is bounded )
proof end;

theorem Th69: :: JORDAN2C:69  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 W being Subset of (Euclid n)
for a being Real
for P being Subset of (TOP-REAL n) st n >= 2 & W = { q where q is Point of (TOP-REAL n) : |.q.| > a } & P = W holds
( P is connected & not W is bounded )
proof end;

theorem Th70: :: JORDAN2C:70  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 W being Subset of (Euclid n)
for a being Real
for P being Subset of (TOP-REAL n) st n >= 2 & W = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } & P = W holds
( P is connected & not W is bounded )
proof end;

theorem Th71: :: JORDAN2C:71  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 P, P1, Q being Subset of (TOP-REAL n)
for W being Subset of (Euclid n) st P = W & P is connected & not W is bounded & P1 = skl (Down P,(Q ` )) & W misses Q holds
P1 is_outside_component_of Q
proof end;

theorem Th72: :: JORDAN2C:72  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 being Subset of (Euclid n)
for B being non empty Subset of (Euclid n)
for C being Subset of ((Euclid n) | B) st A c= B & A = C & C is bounded holds
A is bounded
proof end;

theorem Th73: :: JORDAN2C:73  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 being Subset of (TOP-REAL n) st A is compact holds
A is Bounded
proof end;

registration
let n be Nat;
cluster compact -> Bounded Element of bool the carrier of (TOP-REAL n);
coherence
for b1 being Subset of (TOP-REAL n) st b1 is compact holds
b1 is Bounded
by Th73;
end;

theorem Th74: :: JORDAN2C:74  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 being Subset of (TOP-REAL n) st 1 <= n & A is Bounded holds
A ` <> {}
proof end;

theorem Th75: :: JORDAN2C:75  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 r being Real holds
( ex B being Subset of (Euclid n) st B = { q where q is Point of (TOP-REAL n) : |.q.| < r } & ( for A being Subset of (Euclid n) st A = { q1 where q1 is Point of (TOP-REAL n) : |.q1.| < r } holds
A is bounded ) )
proof end;

theorem Th76: :: JORDAN2C:76  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 being Subset of (TOP-REAL n) st n >= 2 & A is Bounded holds
ex B being Subset of (TOP-REAL n) st
( B is_outside_component_of A & B = UBD A )
proof end;

theorem Th77: :: JORDAN2C:77  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 being Real
for P being Subset of (TOP-REAL n) st P = { q where q is Point of (TOP-REAL n) : |.q.| < a } holds
P is convex
proof end;

theorem Th78: :: JORDAN2C:78  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 u being Point of (Euclid n)
for a being Real
for P being Subset of (TOP-REAL n) st P = Ball u,a holds
P is convex
proof end;

theorem Th79: :: JORDAN2C:79  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 being Real
for P being Subset of (TOP-REAL n) st P = { q where q is Point of (TOP-REAL n) : |.q.| < a } holds
P is connected
proof end;

theorem Th80: :: JORDAN2C:80  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 r being Real
for p, q being Point of (TOP-REAL n)
for u being Point of (Euclid n) st p <> q & p in Ball u,r & q in Ball u,r holds
ex h being Function of I[01] ,(TOP-REAL n) st
( h is continuous & h . 0 = p & h . 1 = q & rng h c= Ball u,r )
proof end;

theorem Th81: :: JORDAN2C:81  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 r being Real
for p1, p2, p being Point of (TOP-REAL n)
for u being Point of (Euclid n)
for f being Function of I[01] ,(TOP-REAL n) st f is continuous & f . 0 = p1 & f . 1 = p2 & p in Ball u,r & p2 in Ball u,r holds
ex h being Function of I[01] ,(TOP-REAL n) st
( h is continuous & h . 0 = p1 & h . 1 = p & rng h c= (rng f) \/ (Ball u,r) )
proof end;

theorem Th82: :: JORDAN2C:82  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 r being Real
for p1, p2, p being Point of (TOP-REAL n)
for u being Point of (Euclid n)
for P being Subset of (TOP-REAL n)
for f being Function of I[01] ,(TOP-REAL n) st f is continuous & rng f c= P & f . 0 = p1 & f . 1 = p2 & p in Ball u,r & p2 in Ball u,r & Ball u,r c= P holds
ex f1 being Function of I[01] ,(TOP-REAL n) st
( f1 is continuous & rng f1 c= P & f1 . 0 = p1 & f1 . 1 = p )
proof end;

theorem Th83: :: JORDAN2C:83  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 R being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n)
for P being Subset of (TOP-REAL n) st R is connected & R is open & P = { q where q is Point of (TOP-REAL n) : ( q <> p & q in R & ( for f being Function of I[01] ,(TOP-REAL n) holds
( not f is continuous or not rng f c= R or not f . 0 = p or not f . 1 = q ) ) )
}
holds
P is open
proof end;

theorem Th84: :: JORDAN2C:84  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 p being Point of (TOP-REAL n)
for R, P being Subset of (TOP-REAL n) st R is connected & R is open & p in R & P = { q where q is Point of (TOP-REAL n) : ( q = p or ex f being Function of I[01] ,(TOP-REAL n) st
( f is continuous & rng f c= R & f . 0 = p & f . 1 = q ) )
}
holds
P is open
proof end;

theorem Th85: :: JORDAN2C:85  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 p being Point of (TOP-REAL n)
for P, R being Subset of (TOP-REAL n) st p in R & P = { q where q is Point of (TOP-REAL n) : ( q = p or ex f being Function of I[01] ,(TOP-REAL n) st
( f is continuous & rng f c= R & f . 0 = p & f . 1 = q ) )
}
holds
P c= R
proof end;

theorem Th86: :: JORDAN2C:86  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 P, R being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) st R is connected & R is open & p in R & P = { q where q is Point of (TOP-REAL n) : ( q = p or ex f being Function of I[01] ,(TOP-REAL n) st
( f is continuous & rng f c= R & f . 0 = p & f . 1 = q ) )
}
holds
R c= P
proof end;

theorem Th87: :: JORDAN2C:87  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 R being Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n) st R is connected & R is open & p in R & q in R & p <> q holds
ex f being Function of I[01] ,(TOP-REAL n) st
( f is continuous & rng f c= R & f . 0 = p & f . 1 = q )
proof end;

theorem Th88: :: JORDAN2C:88  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 being Subset of (TOP-REAL n)
for a being real number st A = { q where q is Point of (TOP-REAL n) : |.q.| = a } holds
( A ` is open & A is closed )
proof end;

theorem Th89: :: JORDAN2C:89  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 B being non empty Subset of (TOP-REAL n) st B is open holds
(TOP-REAL n) | B is locally_connected
proof end;

theorem Th90: :: JORDAN2C:90  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 B being non empty Subset of (TOP-REAL n)
for A being Subset of (TOP-REAL n)
for a being real number st A = { q where q is Point of (TOP-REAL n) : |.q.| = a } & A ` = B holds
(TOP-REAL n) | B is locally_connected
proof end;

theorem Th91: :: JORDAN2C:91  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 f being Function of (TOP-REAL n),R^1 st ( for q being Point of (TOP-REAL n) holds f . q = |.q.| ) holds
f is continuous
proof end;

theorem Th92: :: JORDAN2C:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat ex f being Function of (TOP-REAL n),R^1 st
( ( for q being Point of (TOP-REAL n) holds f . q = |.q.| ) & f is continuous )
proof end;

definition
let X, Y be non empty 1-sorted ;
let f be Function of X,Y;
let x be set ;
assume A1: x is Point of X ;
canceled;
func pi f,x -> Point of Y equals :Def10: :: JORDAN2C:def 10
f . x;
coherence
f . x is Point of Y
proof end;
end;

:: deftheorem JORDAN2C:def 9 :
canceled;

:: deftheorem Def10 defines pi JORDAN2C:def 10 :
for X, Y being non empty 1-sorted
for f being Function of X,Y
for x being set st x is Point of X holds
pi f,x = f . x;

theorem Th93: :: JORDAN2C:93  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 g being Function of I[01] ,(TOP-REAL n) st g is continuous holds
ex f being Function of I[01] ,R^1 st
( ( for t being Point of I[01] holds f . t = |.(g . t).| ) & f is continuous )
proof end;

theorem Th94: :: JORDAN2C:94  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 g being Function of I[01] ,(TOP-REAL n)
for a being Real st g is continuous & |.(pi g,0).| <= a & a <= |.(pi g,1).| holds
ex s being Point of I[01] st |.(pi g,s).| = a
proof end;

theorem Th95: :: JORDAN2C:95  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 r being Real
for q being Point of (TOP-REAL n) st q = <*r*> holds
|.q.| = abs r
proof end;

theorem :: JORDAN2C:96  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 being Subset of (TOP-REAL n)
for a being Real st n >= 1 & a > 0 & A = { q where q is Point of (TOP-REAL n) : |.q.| = a } holds
ex B being Subset of (TOP-REAL n) st
( B is_inside_component_of A & B = BDD A )
proof end;

theorem Th97: :: JORDAN2C:97  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( len (GoB (SpStSeq D)) = 2 & width (GoB (SpStSeq D)) = 2 & (SpStSeq D) /. 1 = (GoB (SpStSeq D)) * 1,2 & (SpStSeq D) /. 2 = (GoB (SpStSeq D)) * 2,2 & (SpStSeq D) /. 3 = (GoB (SpStSeq D)) * 2,1 & (SpStSeq D) /. 4 = (GoB (SpStSeq D)) * 1,1 & (SpStSeq D) /. 5 = (GoB (SpStSeq D)) * 1,2 )
proof end;

theorem Th98: :: JORDAN2C:98  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) holds not LeftComp (SpStSeq D) is Bounded
proof end;

theorem Th99: :: JORDAN2C:99  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) holds LeftComp (SpStSeq D) c= UBD (L~ (SpStSeq D))
proof end;

theorem Th100: :: JORDAN2C:100  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being TopSpace
for A, B, C being Subset of G st A is_a_component_of G & B is_a_component_of G & C is connected & A meets C & B meets C holds
A = B
proof end;

theorem Th101: :: JORDAN2C:101  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for B being Subset of (TOP-REAL 2) st B is_a_component_of (L~ (SpStSeq D)) ` & not B is Bounded holds
B = LeftComp (SpStSeq D)
proof end;

theorem Th102: :: JORDAN2C:102  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( RightComp (SpStSeq D) c= BDD (L~ (SpStSeq D)) & RightComp (SpStSeq D) is Bounded )
proof end;

theorem Th103: :: JORDAN2C:103  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( LeftComp (SpStSeq D) = UBD (L~ (SpStSeq D)) & RightComp (SpStSeq D) = BDD (L~ (SpStSeq D)) )
proof end;

theorem Th104: :: JORDAN2C:104  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( UBD (L~ (SpStSeq D)) <> {} & UBD (L~ (SpStSeq D)) is_outside_component_of L~ (SpStSeq D) & BDD (L~ (SpStSeq D)) <> {} & BDD (L~ (SpStSeq D)) is_inside_component_of L~ (SpStSeq D) )
proof end;

theorem Th105: :: JORDAN2C:105  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty TopSpace
for A being Subset of G st A ` <> {} holds
( A is boundary iff for x being set
for V being Subset of G st x in A & x in V & V is open holds
ex B being Subset of G st
( B is_a_component_of A ` & V meets B ) )
proof end;

theorem Th106: :: JORDAN2C:106  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Subset of (TOP-REAL 2) st A ` <> {} holds
( ( A is boundary & A is Jordan ) iff ex A1, A2 being Subset of (TOP-REAL 2) st
( A ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A = (Cl A1) \ A1 & ( for C1, C2 being Subset of ((TOP-REAL 2) | (A ` )) st C1 = A1 & C2 = A2 holds
( C1 is_a_component_of (TOP-REAL 2) | (A ` ) & C2 is_a_component_of (TOP-REAL 2) | (A ` ) ) ) ) )
proof end;

theorem Th107: :: JORDAN2C:107  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 p being Point of (TOP-REAL n)
for P being Subset of (TOP-REAL n) st n >= 1 & P = {p} holds
P is boundary
proof end;

theorem Th108: :: JORDAN2C:108  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Point of (TOP-REAL 2)
for r being Real st p `1 = q `2 & - (p `2 ) = q `1 & p = r * q holds
( p `1 = 0 & p `2 = 0 & p = 0.REAL 2 )
proof end;

theorem Th109: :: JORDAN2C:109  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q1, q2 being Point of (TOP-REAL 2) holds LSeg q1,q2 is boundary
proof end;

registration
let q1, q2 be Point of (TOP-REAL 2);
cluster LSeg q1,q2 -> boundary ;
coherence
LSeg q1,q2 is boundary
by Th109;
end;

theorem Th110: :: JORDAN2C:110  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2) holds L~ f is boundary
proof end;

registration
let f be FinSequence of (TOP-REAL 2);
cluster L~ f -> boundary Bounded ;
coherence
L~ f is boundary
by Th110;
end;

theorem Th111: :: JORDAN2C:111  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 r being Real
for ep being Point of (Euclid n)
for p, q being Point of (TOP-REAL n) st p = ep & q in Ball ep,r holds
( |.(p - q).| < r & |.(q - p).| < r )
proof end;

theorem :: JORDAN2C:112  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for a being Real
for p being Point of (TOP-REAL 2) st a > 0 & p in L~ (SpStSeq D) holds
ex q being Point of (TOP-REAL 2) st
( q in UBD (L~ (SpStSeq D)) & |.(p - q).| < a )
proof end;

theorem Th113: :: JORDAN2C:113  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
REAL 0 = {(0.REAL 0)}
proof end;

theorem Th114: :: JORDAN2C:114  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 being Subset of (TOP-REAL n) st A is Bounded holds
BDD A is Bounded
proof end;

theorem Th115: :: JORDAN2C:115  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty TopSpace
for A, B, C, D being Subset of G st A is_a_component_of G & B is_a_component_of G & C is_a_component_of G & A \/ B = the carrier of G & C misses A holds
C = B
proof end;

theorem Th116: :: JORDAN2C:116  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Subset of (TOP-REAL 2) st A is Bounded & A is Jordan holds
BDD A is_inside_component_of A
proof end;

theorem :: JORDAN2C:117  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for a being Real
for p being Point of (TOP-REAL 2) st a > 0 & p in L~ (SpStSeq D) holds
ex q being Point of (TOP-REAL 2) st
( q in BDD (L~ (SpStSeq D)) & |.(p - q).| < a )
proof end;

theorem :: JORDAN2C:118  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non constant standard clockwise_oriented special_circular_sequence
for p being Point of (TOP-REAL 2) st f /. 1 = N-min (L~ f) & p `1 < W-bound (L~ f) holds
p in LeftComp f
proof end;

theorem :: JORDAN2C:119  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non constant standard clockwise_oriented special_circular_sequence
for p being Point of (TOP-REAL 2) st f /. 1 = N-min (L~ f) & p `1 > E-bound (L~ f) holds
p in LeftComp f
proof end;

theorem :: JORDAN2C:120  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non constant standard clockwise_oriented special_circular_sequence
for p being Point of (TOP-REAL 2) st f /. 1 = N-min (L~ f) & p `2 < S-bound (L~ f) holds
p in LeftComp f
proof end;

theorem :: JORDAN2C:121  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non constant standard clockwise_oriented special_circular_sequence
for p being Point of (TOP-REAL 2) st f /. 1 = N-min (L~ f) & p `2 > N-bound (L~ f) holds
p in LeftComp f
proof end;