begin
set T2 = TOP-REAL 2;
Lm1:
for A, B, C, Z being set st A c= Z & B c= Z & C c= Z holds
(A \/ B) \/ C c= Z
Lm2:
for A, B, C, D, Z being set st A c= Z & B c= Z & C c= Z & D c= Z holds
((A \/ B) \/ C) \/ D c= Z
Lm3:
for A, B, C, D, Z being set st A misses Z & B misses Z & C misses Z & D misses Z holds
((A \/ B) \/ C) \/ D misses Z
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem
theorem
theorem
theorem Th8:
theorem
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem
Lm4:
for p being Point of (TOP-REAL 2)
for C being Simple_closed_curve
for U being Subset of ((TOP-REAL 2) | (C `)) st p in C holds
{p} misses U
set C0 = Closed-Interval-TSpace (0,1);
set C1 = Closed-Interval-TSpace ((- 1),1);
set l0 = (#) ((- 1),1);
set l1 = ((- 1),1) (#) ;
set h1 = L[01] (((#) ((- 1),1)),(((- 1),1) (#)));
Lm5:
the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] = [: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):]
by BORSUK_1:def 5;
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem
begin
theorem
theorem Th29:
theorem Th30:
Lm7:
for T being non empty TopSpace
for a, b being Point of T
for f being Path of a,b st a,b are_connected holds
rng f c= rng (- f)
theorem Th31:
theorem Th32:
theorem Th33:
theorem
theorem Th35:
theorem
theorem Th37:
theorem
theorem Th39:
theorem Th40:
Lm8:
for T being non empty TopSpace
for a, b, c, d, e being Point of T
for f being Path of a,b
for g being Path of b,c
for h being Path of c,d
for i being Path of d,e st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected holds
rng (((f + g) + h) + i) = (((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)
Lm9:
for T being non empty pathwise_connected TopSpace
for a, b, c, d, e being Point of T
for f being Path of a,b
for g being Path of b,c
for h being Path of c,d
for i being Path of d,e holds rng (((f + g) + h) + i) = (((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)
Lm10:
for T being non empty TopSpace
for a, b, c, d, e, z being Point of T
for f being Path of a,b
for g being Path of b,c
for h being Path of c,d
for i being Path of d,e
for j being Path of e,z st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected & e,z are_connected holds
rng ((((f + g) + h) + i) + j) = ((((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)) \/ (rng j)
Lm11:
for T being non empty pathwise_connected TopSpace
for a, b, c, d, e, z being Point of T
for f being Path of a,b
for g being Path of b,c
for h being Path of c,d
for i being Path of d,e
for j being Path of e,z holds rng ((((f + g) + h) + i) + j) = ((((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)) \/ (rng j)
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
begin
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
for
a,
b,
c,
d being
real number holds
(closed_inside_of_rectangle (a,b,c,d)) /\ (inside_of_rectangle (a,b,c,d)) = inside_of_rectangle (
a,
b,
c,
d)
theorem Th50:
theorem Th51:
for
a,
b,
c,
d being
real number st
a <= b &
c <= d holds
(closed_inside_of_rectangle (a,b,c,d)) \ (inside_of_rectangle (a,b,c,d)) = rectangle (
a,
b,
c,
d)
theorem Th52:
theorem
theorem
theorem
theorem
theorem Th57:
for
a,
b,
c,
d being
real number for
p1,
p2 being
Point of
(TOP-REAL 2) for
P being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 in closed_inside_of_rectangle (
a,
b,
c,
d) & not
p2 in closed_inside_of_rectangle (
a,
b,
c,
d) &
P is_an_arc_of p1,
p2 holds
Segment (
P,
p1,
p2,
p1,
(First_Point (P,p1,p2,(rectangle (a,b,c,d)))))
c= closed_inside_of_rectangle (
a,
b,
c,
d)
begin
definition
let o be
Point of
(TOP-REAL 2);
func diffX2_1 o -> RealMap of
[:(TOP-REAL 2),(TOP-REAL 2):] means :
Def1:
for
x being
Point of
[:(TOP-REAL 2),(TOP-REAL 2):] holds
it . x = ((x `2) `1) - (o `1);
existence
ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `2) `1) - (o `1)
uniqueness
for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `2) `1) - (o `1) ) & ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . x = ((x `2) `1) - (o `1) ) holds
b1 = b2
func diffX2_2 o -> RealMap of
[:(TOP-REAL 2),(TOP-REAL 2):] means :
Def2:
for
x being
Point of
[:(TOP-REAL 2),(TOP-REAL 2):] holds
it . x = ((x `2) `2) - (o `2);
existence
ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `2) `2) - (o `2)
uniqueness
for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `2) `2) - (o `2) ) & ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . x = ((x `2) `2) - (o `2) ) holds
b1 = b2
end;
:: deftheorem Def1 defines diffX2_1 JORDAN:def 1 :
for o being Point of (TOP-REAL 2)
for b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] holds
( b2 = diffX2_1 o iff for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . x = ((x `2) `1) - (o `1) );
:: deftheorem Def2 defines diffX2_2 JORDAN:def 2 :
for o being Point of (TOP-REAL 2)
for b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] holds
( b2 = diffX2_2 o iff for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . x = ((x `2) `2) - (o `2) );
definition
func diffX1_X2_1 -> RealMap of
[:(TOP-REAL 2),(TOP-REAL 2):] means :
Def3:
for
x being
Point of
[:(TOP-REAL 2),(TOP-REAL 2):] holds
it . x = ((x `1) `1) - ((x `2) `1);
existence
ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `1) `1) - ((x `2) `1)
uniqueness
for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `1) `1) - ((x `2) `1) ) & ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . x = ((x `1) `1) - ((x `2) `1) ) holds
b1 = b2
func diffX1_X2_2 -> RealMap of
[:(TOP-REAL 2),(TOP-REAL 2):] means :
Def4:
for
x being
Point of
[:(TOP-REAL 2),(TOP-REAL 2):] holds
it . x = ((x `1) `2) - ((x `2) `2);
existence
ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `1) `2) - ((x `2) `2)
uniqueness
for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `1) `2) - ((x `2) `2) ) & ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . x = ((x `1) `2) - ((x `2) `2) ) holds
b1 = b2
func Proj2_1 -> RealMap of
[:(TOP-REAL 2),(TOP-REAL 2):] means :
Def5:
for
x being
Point of
[:(TOP-REAL 2),(TOP-REAL 2):] holds
it . x = (x `2) `1 ;
existence
ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = (x `2) `1
uniqueness
for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = (x `2) `1 ) & ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . x = (x `2) `1 ) holds
b1 = b2
func Proj2_2 -> RealMap of
[:(TOP-REAL 2),(TOP-REAL 2):] means :
Def6:
for
x being
Point of
[:(TOP-REAL 2),(TOP-REAL 2):] holds
it . x = (x `2) `2 ;
existence
ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = (x `2) `2
uniqueness
for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = (x `2) `2 ) & ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . x = (x `2) `2 ) holds
b1 = b2
end;
:: deftheorem Def3 defines diffX1_X2_1 JORDAN:def 3 :
for b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] holds
( b1 = diffX1_X2_1 iff for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `1) `1) - ((x `2) `1) );
:: deftheorem Def4 defines diffX1_X2_2 JORDAN:def 4 :
for b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] holds
( b1 = diffX1_X2_2 iff for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `1) `2) - ((x `2) `2) );
:: deftheorem Def5 defines Proj2_1 JORDAN:def 5 :
for b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] holds
( b1 = Proj2_1 iff for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = (x `2) `1 );
:: deftheorem Def6 defines Proj2_2 JORDAN:def 6 :
for b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] holds
( b1 = Proj2_2 iff for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = (x `2) `2 );
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
definition
let n be non
empty Element of
NAT ;
let o,
p be
Point of
(TOP-REAL n);
let r be
positive real number ;
assume A1:
p is
Point of
(Tdisk (o,r))
;
set X =
(TOP-REAL n) | ((cl_Ball (o,r)) \ {p});
func DiskProj (
o,
r,
p)
-> Function of
((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})),
(Tcircle (o,r)) means :
Def7:
for
x being
Point of
((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) ex
y being
Point of
(TOP-REAL n) st
(
x = y &
it . x = HC (
p,
y,
o,
r) );
existence
ex b1 being Function of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})),(Tcircle (o,r)) st
for x being Point of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) ex y being Point of (TOP-REAL n) st
( x = y & b1 . x = HC (p,y,o,r) )
uniqueness
for b1, b2 being Function of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})),(Tcircle (o,r)) st ( for x being Point of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) ex y being Point of (TOP-REAL n) st
( x = y & b1 . x = HC (p,y,o,r) ) ) & ( for x being Point of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) ex y being Point of (TOP-REAL n) st
( x = y & b2 . x = HC (p,y,o,r) ) ) holds
b1 = b2
end;
:: deftheorem Def7 defines DiskProj JORDAN:def 7 :
for n being non empty Element of NAT
for o, p being Point of (TOP-REAL n)
for r being positive real number st p is Point of (Tdisk (o,r)) holds
for b5 being Function of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})),(Tcircle (o,r)) holds
( b5 = DiskProj (o,r,p) iff for x being Point of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) ex y being Point of (TOP-REAL n) st
( x = y & b5 . x = HC (p,y,o,r) ) );
theorem Th64:
theorem Th65:
definition
let n be non
empty Element of
NAT ;
let o,
p be
Point of
(TOP-REAL n);
let r be
positive real number ;
assume A1:
p in Ball (
o,
r)
;
set X =
Tcircle (
o,
r);
func RotateCircle (
o,
r,
p)
-> Function of
(Tcircle (o,r)),
(Tcircle (o,r)) means :
Def8:
for
x being
Point of
(Tcircle (o,r)) ex
y being
Point of
(TOP-REAL n) st
(
x = y &
it . x = HC (
y,
p,
o,
r) );
existence
ex b1 being Function of (Tcircle (o,r)),(Tcircle (o,r)) st
for x being Point of (Tcircle (o,r)) ex y being Point of (TOP-REAL n) st
( x = y & b1 . x = HC (y,p,o,r) )
uniqueness
for b1, b2 being Function of (Tcircle (o,r)),(Tcircle (o,r)) st ( for x being Point of (Tcircle (o,r)) ex y being Point of (TOP-REAL n) st
( x = y & b1 . x = HC (y,p,o,r) ) ) & ( for x being Point of (Tcircle (o,r)) ex y being Point of (TOP-REAL n) st
( x = y & b2 . x = HC (y,p,o,r) ) ) holds
b1 = b2
end;
:: deftheorem Def8 defines RotateCircle JORDAN:def 8 :
for n being non empty Element of NAT
for o, p being Point of (TOP-REAL n)
for r being positive real number st p in Ball (o,r) holds
for b5 being Function of (Tcircle (o,r)),(Tcircle (o,r)) holds
( b5 = RotateCircle (o,r,p) iff for x being Point of (Tcircle (o,r)) ex y being Point of (TOP-REAL n) st
( x = y & b5 . x = HC (y,p,o,r) ) );
theorem Th66:
theorem Th67:
begin
theorem Th68:
theorem Th69:
Lm12:
for p1, p2, p being Point of (TOP-REAL 2)
for A being Subset of (TOP-REAL 2)
for r being non negative real number st A is_an_arc_of p1,p2 & A is Subset of (Tdisk (p,r)) holds
ex f being Function of (Tdisk (p,r)),((TOP-REAL 2) | A) st
( f is continuous & f | A = id A )
Lm13:
for p1, p2, p being Point of (TOP-REAL 2)
for C being Simple_closed_curve
for A, P, B being Subset of (TOP-REAL 2)
for U being Subset of ((TOP-REAL 2) | (C `))
for r being positive real number st A is_an_arc_of p1,p2 & A c= C & C c= Ball (p,r) & p in U & (Cl P) /\ (P `) c= A & P c= Ball (p,r) holds
for f being Function of (Tdisk (p,r)),((TOP-REAL 2) | A) st f is continuous & f | A = id A & U = P & U is a_component & B = (cl_Ball (p,r)) \ {p} holds
ex g being Function of (Tdisk (p,r)),((TOP-REAL 2) | B) st
( g is continuous & ( for x being Point of (Tdisk (p,r)) holds
( ( x in Cl P implies g . x = f . x ) & ( x in P ` implies g . x = x ) ) ) )
Lm14:
for p being Point of (TOP-REAL 2)
for C being Simple_closed_curve
for P, B being Subset of (TOP-REAL 2)
for U, V being Subset of ((TOP-REAL 2) | (C `))
for A being non empty Subset of (TOP-REAL 2) st U <> V holds
for r being positive real number st A c= C & C c= Ball (p,r) & p in V & (Cl P) /\ (P `) c= A & Ball (p,r) meets P holds
for f being Function of (Tdisk (p,r)),((TOP-REAL 2) | A) st f is continuous & f | A = id A & U = P & U is a_component & V is a_component & B = (cl_Ball (p,r)) \ {p} holds
ex g being Function of (Tdisk (p,r)),((TOP-REAL 2) | B) st
( g is continuous & ( for x being Point of (Tdisk (p,r)) holds
( ( x in Cl P implies g . x = x ) & ( x in P ` implies g . x = f . x ) ) ) )
Lm15:
for C being Simple_closed_curve
for P being Subset of (TOP-REAL 2)
for U being Subset of ((TOP-REAL 2) | (C `)) st not BDD C is empty & U = P & U is a_component holds
C = Fr P
set rp = 1;
set rl = - 1;
set rg = 3;
set rd = - 3;
set a = |[(- 1),0]|;
set b = |[1,0]|;
set c = |[0,3]|;
set d = |[0,(- 3)]|;
set lg = |[(- 1),3]|;
set pg = |[1,3]|;
set ld = |[(- 1),(- 3)]|;
set pd = |[1,(- 3)]|;
set R = closed_inside_of_rectangle ((- 1),1,(- 3),3);
set dR = rectangle ((- 1),1,(- 3),3);
set TR = Trectangle ((- 1),1,(- 3),3);
Lm16:
|[(- 1),0]| `1 = - 1
by EUCLID:56;
Lm17:
|[1,0]| `1 = 1
by EUCLID:56;
Lm18:
|[(- 1),0]| `2 = 0
by EUCLID:56;
Lm19:
|[1,0]| `2 = 0
by EUCLID:56;
Lm20:
|[0,3]| `1 = 0
by EUCLID:56;
Lm21:
|[0,3]| `2 = 3
by EUCLID:56;
Lm22:
|[0,(- 3)]| `1 = 0
by EUCLID:56;
Lm23:
|[0,(- 3)]| `2 = - 3
by EUCLID:56;
Lm24:
|[(- 1),3]| `1 = - 1
by EUCLID:56;
Lm25:
|[(- 1),3]| `2 = 3
by EUCLID:56;
Lm26:
|[(- 1),(- 3)]| `1 = - 1
by EUCLID:56;
Lm27:
|[(- 1),(- 3)]| `2 = - 3
by EUCLID:56;
Lm28:
|[1,3]| `1 = 1
by EUCLID:56;
Lm29:
|[1,3]| `2 = 3
by EUCLID:56;
Lm30:
|[1,(- 3)]| `1 = 1
by EUCLID:56;
Lm31:
|[1,(- 3)]| `2 = - 3
by EUCLID:56;
Lm32:
|[(- 1),(- 3)]| = |[(|[(- 1),(- 3)]| `1),(|[(- 1),(- 3)]| `2)]|
by EUCLID:57;
Lm33:
|[(- 1),3]| = |[(|[(- 1),3]| `1),(|[(- 1),3]| `2)]|
by EUCLID:57;
Lm34:
|[1,(- 3)]| = |[(|[1,(- 3)]| `1),(|[1,(- 3)]| `2)]|
by EUCLID:57;
Lm35:
|[1,3]| = |[(|[1,3]| `1),(|[1,3]| `2)]|
by EUCLID:57;
Lm36:
rectangle ((- 1),1,(- 3),3) = ((LSeg (|[(- 1),(- 3)]|,|[(- 1),3]|)) \/ (LSeg (|[(- 1),3]|,|[1,3]|))) \/ ((LSeg (|[1,3]|,|[1,(- 3)]|)) \/ (LSeg (|[1,(- 3)]|,|[(- 1),(- 3)]|)))
by SPPOL_2:def 3;
Lm37:
LSeg (|[(- 1),(- 3)]|,|[(- 1),3]|) c= (LSeg (|[(- 1),(- 3)]|,|[(- 1),3]|)) \/ (LSeg (|[(- 1),3]|,|[1,3]|))
by XBOOLE_1:7;
(LSeg (|[(- 1),(- 3)]|,|[(- 1),3]|)) \/ (LSeg (|[(- 1),3]|,|[1,3]|)) c= rectangle ((- 1),1,(- 3),3)
by Lm36, XBOOLE_1:7;
then Lm38:
LSeg (|[(- 1),(- 3)]|,|[(- 1),3]|) c= rectangle ((- 1),1,(- 3),3)
by Lm37, XBOOLE_1:1;
Lm39:
LSeg (|[(- 1),3]|,|[1,3]|) c= (LSeg (|[(- 1),(- 3)]|,|[(- 1),3]|)) \/ (LSeg (|[(- 1),3]|,|[1,3]|))
by XBOOLE_1:7;
(LSeg (|[(- 1),(- 3)]|,|[(- 1),3]|)) \/ (LSeg (|[(- 1),3]|,|[1,3]|)) c= rectangle ((- 1),1,(- 3),3)
by Lm36, XBOOLE_1:7;
then Lm40:
LSeg (|[(- 1),3]|,|[1,3]|) c= rectangle ((- 1),1,(- 3),3)
by Lm39, XBOOLE_1:1;
Lm41:
LSeg (|[1,3]|,|[1,(- 3)]|) c= (LSeg (|[1,3]|,|[1,(- 3)]|)) \/ (LSeg (|[1,(- 3)]|,|[(- 1),(- 3)]|))
by XBOOLE_1:7;
(LSeg (|[1,3]|,|[1,(- 3)]|)) \/ (LSeg (|[1,(- 3)]|,|[(- 1),(- 3)]|)) c= rectangle ((- 1),1,(- 3),3)
by Lm36, XBOOLE_1:7;
then Lm42:
LSeg (|[1,3]|,|[1,(- 3)]|) c= rectangle ((- 1),1,(- 3),3)
by Lm41, XBOOLE_1:1;
Lm43:
LSeg (|[1,(- 3)]|,|[(- 1),(- 3)]|) c= (LSeg (|[1,3]|,|[1,(- 3)]|)) \/ (LSeg (|[1,(- 3)]|,|[(- 1),(- 3)]|))
by XBOOLE_1:7;
(LSeg (|[1,3]|,|[1,(- 3)]|)) \/ (LSeg (|[1,(- 3)]|,|[(- 1),(- 3)]|)) c= rectangle ((- 1),1,(- 3),3)
by Lm36, XBOOLE_1:7;
then Lm44:
LSeg (|[1,(- 3)]|,|[(- 1),(- 3)]|) c= rectangle ((- 1),1,(- 3),3)
by Lm43, XBOOLE_1:1;
Lm45:
LSeg (|[(- 1),(- 3)]|,|[(- 1),3]|) is vertical
by Lm24, Lm26, SPPOL_1:37;
Lm46:
LSeg (|[1,(- 3)]|,|[1,3]|) is vertical
by Lm28, Lm30, SPPOL_1:37;
Lm47:
LSeg (|[(- 1),0]|,|[(- 1),3]|) is vertical
by Lm16, Lm24, SPPOL_1:37;
Lm48:
LSeg (|[(- 1),0]|,|[(- 1),(- 3)]|) is vertical
by Lm16, Lm26, SPPOL_1:37;
Lm49:
LSeg (|[1,0]|,|[1,3]|) is vertical
by Lm17, Lm28, SPPOL_1:37;
Lm50:
LSeg (|[1,0]|,|[1,(- 3)]|) is vertical
by Lm17, Lm30, SPPOL_1:37;
Lm51:
LSeg (|[(- 1),(- 3)]|,|[0,(- 3)]|) is horizontal
by Lm23, Lm27, SPPOL_1:36;
Lm52:
LSeg (|[1,(- 3)]|,|[0,(- 3)]|) is horizontal
by Lm23, Lm31, SPPOL_1:36;
Lm53:
LSeg (|[(- 1),3]|,|[0,3]|) is horizontal
by Lm21, Lm25, SPPOL_1:36;
Lm54:
LSeg (|[1,3]|,|[0,3]|) is horizontal
by Lm21, Lm29, SPPOL_1:36;
Lm55:
LSeg (|[(- 1),3]|,|[1,3]|) is horizontal
by Lm25, Lm29, SPPOL_1:36;
Lm56:
LSeg (|[(- 1),(- 3)]|,|[1,(- 3)]|) is horizontal
by Lm27, Lm31, SPPOL_1:36;
Lm57:
LSeg (|[(- 1),0]|,|[(- 1),3]|) c= LSeg (|[(- 1),(- 3)]|,|[(- 1),3]|)
by Lm16, Lm18, Lm25, Lm26, Lm27, Lm45, Lm47, GOBOARD7:65;
Lm58:
LSeg (|[(- 1),0]|,|[(- 1),(- 3)]|) c= LSeg (|[(- 1),(- 3)]|,|[(- 1),3]|)
by Lm18, Lm25, Lm26, Lm27, Lm45, Lm48, GOBOARD7:65;
Lm59:
LSeg (|[1,0]|,|[1,3]|) c= LSeg (|[1,(- 3)]|,|[1,3]|)
by Lm17, Lm19, Lm29, Lm30, Lm31, Lm46, Lm49, GOBOARD7:65;
Lm60:
LSeg (|[1,0]|,|[1,(- 3)]|) c= LSeg (|[1,(- 3)]|,|[1,3]|)
by Lm19, Lm29, Lm30, Lm31, Lm46, Lm50, GOBOARD7:65;
Lm61:
rectangle ((- 1),1,(- 3),3) = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & p `2 <= 3 & p `2 >= - 3 ) or ( p `1 <= 1 & p `1 >= - 1 & p `2 = 3 ) or ( p `1 <= 1 & p `1 >= - 1 & p `2 = - 3 ) or ( p `1 = 1 & p `2 <= 3 & p `2 >= - 3 ) ) }
by SPPOL_2:58;
then Lm62:
|[0,3]| in rectangle ((- 1),1,(- 3),3)
by Lm20, Lm21;
Lm63:
|[0,(- 3)]| in rectangle ((- 1),1,(- 3),3)
by Lm22, Lm23, Lm61;
Lm64:
(2 + 1) ^2 = (4 + 4) + 1
;
then Lm65:
sqrt 9 = 3
by SQUARE_1:def 4;
Lm66: dist (|[(- 1),0]|,|[1,0]|) =
sqrt ((((|[(- 1),0]| `1) - (|[1,0]| `1)) ^2) + (((|[(- 1),0]| `2) - (|[1,0]| `2)) ^2))
by TOPREAL6:101
.=
- (- 2)
by Lm16, Lm17, Lm18, Lm19, SQUARE_1:90
;
theorem Th70:
theorem Th71:
Lm67:
rectangle ((- 1),1,(- 3),3) c= closed_inside_of_rectangle ((- 1),1,(- 3),3)
by Th45;
Lm68:
|[(- 1),3]| `2 = |[(- 1),3]| `2
;
Lm69:
|[(- 1),3]| `1 <= |[0,3]| `1
by Lm24, EUCLID:56;
|[0,3]| `1 <= |[1,3]| `1
by Lm28, EUCLID:56;
then
LSeg (|[(- 1),3]|,|[0,3]|) c= LSeg (|[(- 1),3]|,|[1,3]|)
by Lm53, Lm55, Lm68, Lm69, GOBOARD7:66;
then Lm70:
LSeg (|[(- 1),3]|,|[0,3]|) c= rectangle ((- 1),1,(- 3),3)
by Lm40, XBOOLE_1:1;
LSeg (|[1,3]|,|[0,3]|) c= LSeg (|[(- 1),3]|,|[1,3]|)
by Lm20, Lm21, Lm24, Lm25, Lm28, Lm54, Lm55, GOBOARD7:66;
then Lm71:
LSeg (|[1,3]|,|[0,3]|) c= rectangle ((- 1),1,(- 3),3)
by Lm40, XBOOLE_1:1;
Lm72:
|[(- 1),(- 3)]| `2 = |[(- 1),(- 3)]| `2
;
Lm73:
|[(- 1),(- 3)]| `1 <= |[0,(- 3)]| `1
by Lm26, EUCLID:56;
|[0,(- 3)]| `1 <= |[1,(- 3)]| `1
by Lm30, EUCLID:56;
then
LSeg (|[(- 1),(- 3)]|,|[0,(- 3)]|) c= LSeg (|[(- 1),(- 3)]|,|[1,(- 3)]|)
by Lm51, Lm56, Lm72, Lm73, GOBOARD7:66;
then Lm74:
LSeg (|[(- 1),(- 3)]|,|[0,(- 3)]|) c= rectangle ((- 1),1,(- 3),3)
by Lm44, XBOOLE_1:1;
LSeg (|[1,(- 3)]|,|[0,(- 3)]|) c= LSeg (|[(- 1),(- 3)]|,|[1,(- 3)]|)
by Lm22, Lm23, Lm26, Lm27, Lm30, Lm52, Lm56, GOBOARD7:66;
then Lm75:
LSeg (|[1,(- 3)]|,|[0,(- 3)]|) c= rectangle ((- 1),1,(- 3),3)
by Lm44, XBOOLE_1:1;
Lm76:
for p being Point of (TOP-REAL 2) st 0 <= p `2 & p in rectangle ((- 1),1,(- 3),3) & not p in LSeg (|[(- 1),0]|,|[(- 1),3]|) & not p in LSeg (|[(- 1),3]|,|[0,3]|) & not p in LSeg (|[0,3]|,|[1,3]|) holds
p in LSeg (|[1,3]|,|[1,0]|)
Lm77:
for p being Point of (TOP-REAL 2) st p `2 <= 0 & p in rectangle ((- 1),1,(- 3),3) & not p in LSeg (|[(- 1),0]|,|[(- 1),(- 3)]|) & not p in LSeg (|[(- 1),(- 3)]|,|[0,(- 3)]|) & not p in LSeg (|[0,(- 3)]|,|[1,(- 3)]|) holds
p in LSeg (|[1,(- 3)]|,|[1,0]|)
theorem Th72:
theorem Th73:
theorem Th74:
Lm78:
for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C holds
LSeg (|[(- 1),3]|,|[0,3]|) misses C
Lm79:
for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C holds
LSeg (|[1,3]|,|[0,3]|) misses C
Lm80:
for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C holds
LSeg (|[(- 1),(- 3)]|,|[0,(- 3)]|) misses C
Lm81:
for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C holds
LSeg (|[1,(- 3)]|,|[0,(- 3)]|) misses C
Lm82:
for p being Point of (TOP-REAL 2)
for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C & p in C ` & p in LSeg (|[(- 1),0]|,|[(- 1),3]|) holds
LSeg (p,|[(- 1),3]|) misses C
Lm83:
for p being Point of (TOP-REAL 2)
for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C & p in C ` & p in LSeg (|[1,0]|,|[1,3]|) holds
LSeg (p,|[1,3]|) misses C
Lm84:
for p being Point of (TOP-REAL 2)
for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C & p in C ` & p in LSeg (|[(- 1),0]|,|[(- 1),(- 3)]|) holds
LSeg (p,|[(- 1),(- 3)]|) misses C
Lm85:
for p being Point of (TOP-REAL 2)
for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C & p in C ` & p in LSeg (|[1,0]|,|[1,(- 3)]|) holds
LSeg (p,|[1,(- 3)]|) misses C
Lm86:
for r being real number holds
( not |[0,r]| in rectangle ((- 1),1,(- 3),3) or r = - 3 or r = 3 )
theorem Th75:
theorem Th76:
theorem Th77:
theorem Th78:
theorem Th79:
theorem Th80:
Lm87:
for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in P holds
|[0,3]| `1 = ((W-bound P) + (E-bound P)) / 2
Lm88:
for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in P holds
|[0,(- 3)]| `1 = ((W-bound P) + (E-bound P)) / 2
theorem Th81:
theorem Th82:
theorem Th83:
theorem Th84:
theorem Th85:
theorem Th86:
theorem Th87:
theorem Th88:
theorem Th89:
theorem Th90:
theorem Th91:
theorem
theorem Th93:
Lm89:
for p being Point of (TOP-REAL 2) st p in closed_inside_of_rectangle ((- 1),1,(- 3),3) holds
closed_inside_of_rectangle ((- 1),1,(- 3),3) c= Ball (p,10)
theorem
Lm90:
for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C holds
ex Jc, Jd being compact with_the_max_arc Subset of (TOP-REAL 2) st
( Jc is_an_arc_of |[(- 1),0]|,|[1,0]| & Jd is_an_arc_of |[(- 1),0]|,|[1,0]| & C = Jc \/ Jd & Jc /\ Jd = {|[(- 1),0]|,|[1,0]|} & UMP C in Jc & LMP C in Jd & W-bound C = W-bound Jc & E-bound C = E-bound Jc )
theorem Th95:
for
C being
Simple_closed_curve st
|[(- 1),0]|,
|[1,0]| realize-max-dist-in C holds
for
Jc,
Jd being
compact with_the_max_arc Subset of
(TOP-REAL 2) st
Jc is_an_arc_of |[(- 1),0]|,
|[1,0]| &
Jd is_an_arc_of |[(- 1),0]|,
|[1,0]| &
C = Jc \/ Jd &
Jc /\ Jd = {|[(- 1),0]|,|[1,0]|} &
UMP C in Jc &
LMP C in Jd &
W-bound C = W-bound Jc &
E-bound C = E-bound Jc holds
for
Ux being
Subset of
(TOP-REAL 2) st
Ux = Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) holds
(
Ux is_inside_component_of C & ( for
V being
Subset of
(TOP-REAL 2) st
V is_inside_component_of C holds
V = Ux ) )
theorem Th96:
for
C being
Simple_closed_curve st
|[(- 1),0]|,
|[1,0]| realize-max-dist-in C holds
for
Jc,
Jd being
compact with_the_max_arc Subset of
(TOP-REAL 2) st
Jc is_an_arc_of |[(- 1),0]|,
|[1,0]| &
Jd is_an_arc_of |[(- 1),0]|,
|[1,0]| &
C = Jc \/ Jd &
Jc /\ Jd = {|[(- 1),0]|,|[1,0]|} &
UMP C in Jc &
LMP C in Jd &
W-bound C = W-bound Jc &
E-bound C = E-bound Jc holds
BDD C = Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `)))
Lm91:
for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C holds
C is Jordan
Lm92:
for C being Simple_closed_curve holds C is Jordan
theorem
theorem
theorem