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

registration
cluster -> non trivial Element of K22(the carrier of (TOP-REAL 2));
coherence
for b1 being Simple_closed_curve holds not b1 is trivial
proof end;
end;

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

theorem Th1: :: BORSUK_4:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for A, B being non empty Subset of X st A c< B holds
ex p being Element of X st
( p in B & A c= B \ {p} )
proof end;

theorem Th2: :: BORSUK_4:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for A being non empty Subset of X holds
( A is trivial iff ex x being Element of X st A = {x} )
proof end;

registration
let T be non trivial 1-sorted ;
cluster non trivial Element of K22(the carrier of T);
existence
not for b1 being Subset of T holds b1 is trivial
proof end;
end;

theorem Th3: :: BORSUK_4:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non trivial set
for p being set ex q being Element of X st q <> p
proof end;

registration
let X be non trivial set ;
cluster non trivial Element of K22(X);
existence
not for b1 being Subset of X holds b1 is trivial
proof end;
end;

theorem Th4: :: BORSUK_4:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non trivial set
for X being non trivial Subset of T
for p being set ex q being Element of T st
( q in X & q <> p )
proof end;

theorem Th5: :: BORSUK_4:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being Function
for a being set st f is one-to-one & g is one-to-one & (dom f) /\ (dom g) = {a} & (rng f) /\ (rng g) = {(f . a)} holds
f +* g is one-to-one
proof end;

theorem Th6: :: BORSUK_4:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being Function
for a being set st f is one-to-one & g is one-to-one & (dom f) /\ (dom g) = {a} & (rng f) /\ (rng g) = {(f . a)} & f . a = g . a holds
(f +* g) " = (f " ) +* (g " )
proof end;

theorem Th7: :: BORSUK_4:7  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 p, q being Point of (TOP-REAL n) st A is_an_arc_of p,q holds
not A \ {p} is empty
proof end;

theorem :: BORSUK_4: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 Point of (TOP-REAL n) holds LSeg a,b is convex
proof end;

theorem :: BORSUK_4:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s3, s4, l being real number st s1 <= s3 & s1 < s4 & 0 <= l & l <= 1 holds
s1 <= ((1 - l) * s3) + (l * s4)
proof end;

theorem Th10: :: BORSUK_4:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for a, b being real number holds
( not x in [.a,b.] or x in ].a,b.[ or x = a or x = b )
proof end;

theorem Th11: :: BORSUK_4:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being real number st ].a,b.[ meets [.c,d.] holds
b > c
proof end;

theorem Th12: :: BORSUK_4:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being real number st b <= c holds
[.a,b.] misses ].c,d.[
proof end;

theorem Th13: :: BORSUK_4:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being real number st b <= c holds
].a,b.[ misses [.c,d.]
proof end;

theorem :: BORSUK_4:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being real number st a <= b & [.a,b.] c= [.c,d.] holds
( c <= a & b <= d )
proof end;

theorem Th15: :: BORSUK_4:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being real number st a < b & ].a,b.[ c= [.c,d.] holds
( c <= a & b <= d )
proof end;

theorem :: BORSUK_4:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being real number st a < b & ].a,b.[ c= [.c,d.] holds
[.a,b.] c= [.c,d.]
proof end;

theorem Th17: :: BORSUK_4:17  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 I[01]
for a, b being real number st a < b & A = ].a,b.[ holds
[.a,b.] c= the carrier of I[01]
proof end;

theorem Th18: :: BORSUK_4:18  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 I[01]
for a, b being real number st a < b & A = ].a,b.] holds
[.a,b.] c= the carrier of I[01]
proof end;

theorem Th19: :: BORSUK_4:19  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 I[01]
for a, b being real number st a < b & A = [.a,b.[ holds
[.a,b.] c= the carrier of I[01]
proof end;

theorem Th20: :: BORSUK_4:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a <> b holds
Cl ].a,b.] = [.a,b.]
proof end;

theorem Th21: :: BORSUK_4:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a <> b holds
Cl [.a,b.[ = [.a,b.]
proof end;

theorem :: BORSUK_4:22  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 I[01]
for a, b being real number st a < b & A = ].a,b.[ holds
Cl A = [.a,b.]
proof end;

theorem Th23: :: BORSUK_4:23  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 I[01]
for a, b being real number st a < b & A = ].a,b.] holds
Cl A = [.a,b.]
proof end;

theorem Th24: :: BORSUK_4:24  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 I[01]
for a, b being real number st a < b & A = [.a,b.[ holds
Cl A = [.a,b.]
proof end;

theorem :: BORSUK_4:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a < b holds
[.a,b.] <> ].a,b.]
proof end;

theorem Th26: :: BORSUK_4:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number holds
( [.a,b.[ misses {b} & ].a,b.] misses {a} )
proof end;

Lm1: for a, b being real number holds
( ].a,b.[ misses {b} & ].a,b.[ misses {a} )
proof end;

theorem Th27: :: BORSUK_4:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a <= b holds
[.a,b.] \ {a} = ].a,b.]
proof end;

theorem Th28: :: BORSUK_4:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a <= b holds
[.a,b.] \ {b} = [.a,b.[
proof end;

theorem Th29: :: BORSUK_4:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a < b & b < c holds
].a,b.] /\ [.b,c.[ = {b}
proof end;

theorem Th30: :: BORSUK_4:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number holds
( [.a,b.[ misses [.b,c.] & [.a,b.] misses ].b,c.] )
proof end;

theorem Th31: :: BORSUK_4:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a <= b & b <= c holds
[.a,c.] \ {b} = [.a,b.[ \/ ].b,c.]
proof end;

theorem Th32: :: BORSUK_4:32  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 I[01]
for a, b being real number st a <= b & A = [.a,b.] holds
( 0 <= a & b <= 1 )
proof end;

theorem Th33: :: BORSUK_4:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being Subset of I[01]
for a, b, c being real number st a < b & b < c & A = [.a,b.[ & B = ].b,c.] holds
A,B are_separated
proof end;

theorem Th34: :: BORSUK_4:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a <= b holds
[.a,b.] = [.a,b.[ \/ {b}
proof end;

theorem Th35: :: BORSUK_4:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a <= b holds
[.a,b.] = {a} \/ ].a,b.]
proof end;

theorem Th36: :: BORSUK_4:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being real number st a <= b & b < c & c <= d holds
[.a,d.] = ([.a,b.] \/ ].b,c.[) \/ [.c,d.]
proof end;

theorem Th37: :: BORSUK_4:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being real number st a <= b & b < c & c <= d holds
[.a,d.] \ ([.a,b.] \/ [.c,d.]) = ].b,c.[
proof end;

theorem Th38: :: BORSUK_4:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a < b & b < c holds
].a,b.] \/ ].b,c.[ = ].a,c.[
proof end;

theorem Th39: :: BORSUK_4:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a < b & b < c holds
[.b,c.[ c= ].a,c.[
proof end;

theorem Th40: :: BORSUK_4:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a < b & b < c holds
].a,b.] \/ [.b,c.[ = ].a,c.[
proof end;

theorem Th41: :: BORSUK_4:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a < b & b < c holds
].a,c.[ \ ].a,b.] = ].b,c.[
proof end;

theorem Th42: :: BORSUK_4:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a < b & b < c holds
].a,c.[ \ [.b,c.[ = ].a,b.[
proof end;

theorem :: BORSUK_4:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2 being Point of I[01] holds [.p1,p2.] is Subset of I[01] by BORSUK_1:83, RCOMP_1:16;

theorem Th44: :: BORSUK_4:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Point of I[01] holds ].a,b.[ is Subset of I[01]
proof end;

theorem :: BORSUK_4:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being real number holds {p} is closed-interval Subset of REAL
proof end;

theorem Th46: :: BORSUK_4:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty connected Subset of I[01]
for a, b, c being Point of I[01] st a <= b & b <= c & a in A & c in A holds
b in A
proof end;

theorem Th47: :: BORSUK_4:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty connected Subset of I[01]
for a, b being real number st a in A & b in A holds
[.a,b.] c= A
proof end;

theorem Th48: :: BORSUK_4:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number
for A being Subset of I[01] st A = [.a,b.] holds
A is closed
proof end;

theorem Th49: :: BORSUK_4:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2 being Point of I[01] st p1 <= p2 holds
[.p1,p2.] is non empty connected compact Subset of I[01]
proof end;

theorem Th50: :: BORSUK_4:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of I[01]
for X' being Subset of REAL st X' = X holds
( X' is bounded_above & X' is bounded_below )
proof end;

theorem Th51: :: BORSUK_4:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of I[01]
for X' being Subset of REAL
for x being real number st x in X' & X' = X holds
( inf X' <= x & x <= sup X' )
proof end;

Lm2: I[01] is closed SubSpace of R^1
by TOPMETR:27, TREAL_1:5;

theorem Th52: :: BORSUK_4:52  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 REAL
for B being Subset of I[01] st A = B holds
( A is closed iff B is closed )
proof end;

theorem Th53: :: BORSUK_4:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being closed-interval Subset of REAL holds inf C <= sup C
proof end;

theorem Th54: :: BORSUK_4:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty connected compact Subset of I[01]
for C' being Subset of REAL st C = C' & [.(inf C'),(sup C').] c= C' holds
[.(inf C'),(sup C').] = C'
proof end;

theorem Th55: :: BORSUK_4:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty connected compact Subset of I[01] holds C is closed-interval Subset of REAL
proof end;

theorem Th56: :: BORSUK_4:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty connected compact Subset of I[01] ex p1, p2 being Point of I[01] st
( p1 <= p2 & C = [.p1,p2.] )
proof end;

definition
func I(01) -> non empty strict SubSpace of I[01] means :Def1: :: BORSUK_4:def 1
the carrier of it = ].0,1.[;
existence
ex b1 being non empty strict SubSpace of I[01] st the carrier of b1 = ].0,1.[
proof end;
uniqueness
for b1, b2 being non empty strict SubSpace of I[01] st the carrier of b1 = ].0,1.[ & the carrier of b2 = ].0,1.[ holds
b1 = b2
by TSEP_1:5;
end;

:: deftheorem Def1 defines I(01) BORSUK_4:def 1 :
for b1 being non empty strict SubSpace of I[01] holds
( b1 = I(01) iff the carrier of b1 = ].0,1.[ );

theorem Th57: :: BORSUK_4:57  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 I[01] st A = the carrier of I(01) holds
I(01) = I[01] | A
proof end;

theorem Th58: :: BORSUK_4:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
the carrier of I(01) = the carrier of I[01] \ {0,1}
proof end;

theorem Th59: :: BORSUK_4:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
I(01) is open SubSpace of I[01] by Th58, JORDAN6:41, TSEP_1:def 1;

theorem Th60: :: BORSUK_4:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds
( r in the carrier of I(01) iff ( 0 < r & r < 1 ) )
proof end;

theorem Th61: :: BORSUK_4:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Point of I[01] st a < b & b <> 1 holds
].a,b.] is non empty Subset of I(01)
proof end;

theorem Th62: :: BORSUK_4:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Point of I[01] st a < b & a <> 0 holds
[.a,b.[ is non empty Subset of I(01)
proof end;

theorem :: BORSUK_4:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being Simple_closed_curve holds (TOP-REAL 2) | R^2-unit_square ,(TOP-REAL 2) | D are_homeomorphic
proof end;

theorem :: BORSUK_4:64  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 D being non empty Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st D is_an_arc_of p1,p2 holds
I(01) ,(TOP-REAL n) | (D \ {p1,p2}) are_homeomorphic
proof end;

theorem Th65: :: BORSUK_4:65  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 D being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st D is_an_arc_of p1,p2 holds
I[01] ,(TOP-REAL n) | D are_homeomorphic
proof end;

theorem :: BORSUK_4:66  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 being Point of (TOP-REAL n) st p1 <> p2 holds
I[01] ,(TOP-REAL n) | (LSeg p1,p2) are_homeomorphic
proof end;

theorem Th67: :: BORSUK_4:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being Subset of I(01) st ex p1, p2 being Point of I[01] st
( p1 < p2 & E = [.p1,p2.] ) holds
I[01] ,I(01) | E are_homeomorphic
proof end;

theorem Th68: :: BORSUK_4:68  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 p, q being Point of (TOP-REAL n)
for a, b being Point of I[01] st A is_an_arc_of p,q & a < b holds
ex E being non empty Subset of I[01] ex f being Function of (I[01] | E),((TOP-REAL n) | A) st
( E = [.a,b.] & f is_homeomorphism & f . a = p & f . b = q )
proof end;

theorem Th69: :: BORSUK_4:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being TopSpace
for B being non empty TopSpace
for f being Function of A,B
for C being TopSpace
for X being Subset of A st f is continuous & C is SubSpace of B holds
for h being Function of (A | X),C st h = f | X holds
h is continuous
proof end;

theorem Th70: :: BORSUK_4:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of I[01]
for a, b being Point of I[01] st X = ].a,b.[ holds
X is open
proof end;

theorem Th71: :: BORSUK_4:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of I(01)
for a, b being Point of I[01] st X = ].a,b.[ holds
X is open
proof end;

theorem Th72: :: BORSUK_4:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of I(01)
for a being Point of I[01] st X = ].0,a.] holds
X is closed
proof end;

theorem Th73: :: BORSUK_4:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of I(01)
for a being Point of I[01] st X = [.a,1.[ holds
X is closed
proof end;

theorem Th74: :: BORSUK_4: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)
for p, q being Point of (TOP-REAL n)
for a, b being Point of I[01] st A is_an_arc_of p,q & a < b & b <> 1 holds
ex E being non empty Subset of I(01) ex f being Function of (I(01) | E),((TOP-REAL n) | (A \ {p})) st
( E = ].a,b.] & f is_homeomorphism & f . b = q )
proof end;

theorem Th75: :: BORSUK_4: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 A being Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n)
for a, b being Point of I[01] st A is_an_arc_of p,q & a < b & a <> 0 holds
ex E being non empty Subset of I(01) ex f being Function of (I(01) | E),((TOP-REAL n) | (A \ {q})) st
( E = [.a,b.[ & f is_homeomorphism & f . a = p )
proof end;

theorem Th76: :: BORSUK_4: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, B being Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n) st A is_an_arc_of p,q & B is_an_arc_of q,p & A /\ B = {p,q} & p <> q holds
I(01) ,(TOP-REAL n) | ((A \ {p}) \/ (B \ {p})) are_homeomorphic
proof end;

theorem Th77: :: BORSUK_4:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being Simple_closed_curve
for p being Point of (TOP-REAL 2) st p in D holds
(TOP-REAL 2) | (D \ {p}), I(01) are_homeomorphic
proof end;

theorem :: BORSUK_4:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being Simple_closed_curve
for p, q being Point of (TOP-REAL 2) st p in D & q in D holds
(TOP-REAL 2) | (D \ {p}),(TOP-REAL 2) | (D \ {q}) are_homeomorphic
proof end;

theorem Th79: :: BORSUK_4: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 C being non empty Subset of (TOP-REAL n)
for E being Subset of I(01) st ex p1, p2 being Point of I[01] st
( p1 < p2 & E = [.p1,p2.] ) & I(01) | E,(TOP-REAL n) | C are_homeomorphic holds
ex s1, s2 being Point of (TOP-REAL n) st C is_an_arc_of s1,s2
proof end;

theorem Th80: :: BORSUK_4:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Dp being non empty Subset of (TOP-REAL 2)
for f being Function of ((TOP-REAL 2) | Dp),I(01)
for C being non empty Subset of (TOP-REAL 2) st f is_homeomorphism & C c= Dp & ex p1, p2 being Point of I[01] st
( p1 < p2 & f .: C = [.p1,p2.] ) holds
ex s1, s2 being Point of (TOP-REAL 2) st C is_an_arc_of s1,s2
proof end;

theorem :: BORSUK_4:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being Simple_closed_curve
for C being non empty connected compact Subset of (TOP-REAL 2) holds
( not C c= D or C = D or ex p1, p2 being Point of (TOP-REAL 2) st C is_an_arc_of p1,p2 or ex p being Point of (TOP-REAL 2) st C = {p} )
proof end;

registration
cluster the carrier of I[01] -> real-membered ;
coherence
the carrier of I[01] is real-membered
by BORSUK_1:83;
end;

Lm3: for a, b, r, s being real number st ( a <= b or r <= s ) & [.a,b.] = [.r,s.] holds
( a = r & b = s )
proof end;

theorem Th82: :: BORSUK_4:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of I[01] st C c= ].0,1.[ holds
ex D being closed-interval Subset of REAL st
( C c= D & D c= ].0,1.[ & inf C = inf D & sup C = sup D )
proof end;

theorem Th83: :: BORSUK_4:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of I[01] st C c= ].0,1.[ holds
ex p1, p2 being Point of I[01] st
( p1 <= p2 & C c= [.p1,p2.] & [.p1,p2.] c= ].0,1.[ )
proof end;

theorem :: BORSUK_4:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being Simple_closed_curve
for C being closed Subset of (TOP-REAL 2) st C c= D & C <> D holds
ex p1, p2 being Point of (TOP-REAL 2) ex B being Subset of (TOP-REAL 2) st
( B is_an_arc_of p1,p2 & C c= B & B c= D )
proof end;