let P, Q1 be non empty Subset of (TOP-REAL 2); for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & Q1 is_an_arc_of q1,q2 & LE q1,q2,P,p1,p2 & Q1 c= P holds
Q1 = Segment (P,p1,p2,q1,q2)
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ( P is_an_arc_of p1,p2 & Q1 is_an_arc_of q1,q2 & LE q1,q2,P,p1,p2 & Q1 c= P implies Q1 = Segment (P,p1,p2,q1,q2) )
assume that
A1:
P is_an_arc_of p1,p2
and
A2:
Q1 is_an_arc_of q1,q2
and
A3:
LE q1,q2,P,p1,p2
and
A4:
Q1 c= P
; Q1 = Segment (P,p1,p2,q1,q2)
reconsider Q0 = Segment (P,p1,p2,q1,q2) as non empty Subset of (TOP-REAL 2) by A3, JORDAN16:18;
A5:
q1 <> q2
by A2, JORDAN6:37;
then A6:
Segment (P,p1,p2,q1,q2) is_an_arc_of q1,q2
by A1, A3, JORDAN16:21;
A7:
q2 in P
by A3, JORDAN5C:def 3;
A8:
now not q1 = p2assume A9:
q1 = p2
;
contradiction
LE q2,
p2,
P,
p1,
p2
by A1, A7, JORDAN5C:10;
hence
contradiction
by A1, A2, A3, A9, JORDAN5C:12, JORDAN6:37;
verum end;
A10:
q1 in P
by A3, JORDAN5C:def 3;
A11:
now not q2 = p1assume A12:
q2 = p1
;
contradiction
LE p1,
q1,
P,
p1,
p2
by A1, A10, JORDAN5C:10;
hence
contradiction
by A1, A2, A3, A12, JORDAN5C:12, JORDAN6:37;
verum end;
A13:
( p1 in P & p2 in P )
by A1, TOPREAL1:1;
now Q1 c= Q0A14:
LE p1,
q1,
P,
p1,
p2
by A1, A10, JORDAN5C:10;
then A15:
(Segment (P,p1,p2,p1,q1)) \/ (Segment (P,p1,p2,q1,q2)) = Segment (
P,
p1,
p2,
p1,
q2)
by A1, A3, Th22;
A16:
[#] ((TOP-REAL 2) | P) = P
by PRE_TOPC:def 5;
A17:
LE q2,
p2,
P,
p1,
p2
by A1, A7, JORDAN5C:10;
A18:
[#] I[01] = the
carrier of
I[01]
;
Q0 is_an_arc_of q1,
q2
by A1, A3, A5, JORDAN16:21;
then A19:
q2 in Q0
by TOPREAL1:1;
assume
not
Q1 c= Q0
;
contradictionthen consider x8 being
object such that A20:
x8 in Q1
and A21:
not
x8 in Q0
;
reconsider q =
x8 as
Point of
(TOP-REAL 2) by A20;
A22:
q <> q1
by A3, A21, JORDAN16:5;
LE p1,
q2,
P,
p1,
p2
by A3, A14, JORDAN5C:13;
then (Segment (P,p1,p2,p1,q2)) \/ (Segment (P,p1,p2,q2,p2)) =
Segment (
P,
p1,
p2,
p1,
p2)
by A1, A17, Th22
.=
P
by A1, Th24
;
then A23:
(
q in Segment (
P,
p1,
p2,
p1,
q2) or
q in Segment (
P,
p1,
p2,
q2,
p2) )
by A4, A20, XBOOLE_0:def 3;
now ( ( q in Segment (P,p1,p2,p1,q1) & contradiction ) or ( q in Segment (P,p1,p2,q2,p2) & contradiction ) )per cases
( q in Segment (P,p1,p2,p1,q1) or q in Segment (P,p1,p2,q2,p2) )
by A21, A15, A23, XBOOLE_0:def 3;
case A24:
q in Segment (
P,
p1,
p2,
p1,
q1)
;
contradictionA25:
not
q in {q1}
by A22, TARSKI:def 1;
not
q2 in {q1}
by A5, TARSKI:def 1;
then reconsider Qa =
P \ {q1} as non
empty Subset of
((TOP-REAL 2) | P) by A7, A16, XBOOLE_0:def 5, XBOOLE_1:36;
A26:
the
carrier of
(((TOP-REAL 2) | P) | Qa) = Qa
by PRE_TOPC:8;
reconsider Qa9 =
Qa as
Subset of
(TOP-REAL 2) ;
A27:
the
carrier of
(((TOP-REAL 2) | P) | Qa) = Qa
by PRE_TOPC:8;
A28:
Segment (
Q1,
q1,
q2,
q,
q2)
is_an_arc_of q,
q2
by A2, A20, A21, A19, Th21;
then consider f2 being
Function of
I[01],
((TOP-REAL 2) | (Segment (Q1,q1,q2,q,q2))) such that A29:
f2 is
being_homeomorphism
and A30:
(
f2 . 0 = q &
f2 . 1
= q2 )
by TOPREAL1:def 1;
A31:
rng f2 =
[#] ((TOP-REAL 2) | (Segment (Q1,q1,q2,q,q2)))
by A29, TOPS_2:def 5
.=
Segment (
Q1,
q1,
q2,
q,
q2)
by PRE_TOPC:def 5
;
A32:
( not
p2 in {q1} & not
q2 in {q1} )
by A5, A8, TARSKI:def 1;
q in { p3 where p3 is Point of (TOP-REAL 2) : ( LE p1,p3,P,p1,p2 & LE p3,q1,P,p1,p2 ) }
by A24, JORDAN6:26;
then A33:
ex
p3 being
Point of
(TOP-REAL 2) st
(
q = p3 &
LE p1,
p3,
P,
p1,
p2 &
LE p3,
q1,
P,
p1,
p2 )
;
then
not
p1 in {q1}
by TARSKI:def 1;
then reconsider p19 =
p1,
q9 =
q,
q29 =
q2,
p29 =
p2 as
Point of
(((TOP-REAL 2) | P) | Qa) by A4, A7, A13, A20, A26, A32, A25, XBOOLE_0:def 5;
now ( ( q <> p1 & ex G1 being Path of p19,q9 st
( G1 is continuous & G1 . 0 = p19 & G1 . 1 = q9 ) ) or ( q = p1 & ex G1 being Path of p19,q9 st
( G1 is continuous & G1 . 0 = p19 & G1 . 1 = q9 ) ) )per cases
( q <> p1 or q = p1 )
;
case
q <> p1
;
ex G1 being Path of p19,q9 st
( G1 is continuous & G1 . 0 = p19 & G1 . 1 = q9 )then A36:
Segment (
P,
p1,
p2,
p1,
q)
is_an_arc_of p1,
q
by A1, A4, A20, JORDAN16:24;
then consider f1 being
Function of
I[01],
((TOP-REAL 2) | (Segment (P,p1,p2,p1,q))) such that A37:
f1 is
being_homeomorphism
and A38:
(
f1 . 0 = p1 &
f1 . 1
= q )
by TOPREAL1:def 1;
A39:
rng f1 =
[#] ((TOP-REAL 2) | (Segment (P,p1,p2,p1,q)))
by A37, TOPS_2:def 5
.=
Segment (
P,
p1,
p2,
p1,
q)
by PRE_TOPC:def 5
;
{ p where p is Point of (TOP-REAL 2) : ( LE p1,p,P,p1,p2 & LE p,q,P,p1,p2 ) } c= Qa
proof
let x be
object ;
TARSKI:def 3 ( not x in { p where p is Point of (TOP-REAL 2) : ( LE p1,p,P,p1,p2 & LE p,q,P,p1,p2 ) } or x in Qa )
assume
x in { p where p is Point of (TOP-REAL 2) : ( LE p1,p,P,p1,p2 & LE p,q,P,p1,p2 ) }
;
x in Qa
then A40:
ex
p being
Point of
(TOP-REAL 2) st
(
x = p &
LE p1,
p,
P,
p1,
p2 &
LE p,
q,
P,
p1,
p2 )
;
then
x <> q1
by A1, A22, A33, JORDAN5C:12;
then A41:
not
x in {q1}
by TARSKI:def 1;
x in P
by A40, JORDAN5C:def 3;
hence
x in Qa
by A41, XBOOLE_0:def 5;
verum
end; then A42:
Segment (
P,
p1,
p2,
p1,
q)
c= Qa
by JORDAN6:26;
dom f1 = the
carrier of
I[01]
by A18, A37, TOPS_2:def 5;
then reconsider g1 =
f1 as
Function of
I[01],
(((TOP-REAL 2) | P) | Qa) by A26, A39, A42, FUNCT_2:2;
A43:
f1 is
continuous
by A37, TOPS_2:def 5;
A44:
for
G being
Subset of
(((TOP-REAL 2) | P) | Qa) st
G is
open holds
g1 " G is
open
proof
let G be
Subset of
(((TOP-REAL 2) | P) | Qa);
( G is open implies g1 " G is open )
A45:
((TOP-REAL 2) | P) | Qa = (TOP-REAL 2) | Qa9
by PRE_TOPC:7, XBOOLE_1:36;
assume
G is
open
;
g1 " G is open
then consider G4 being
Subset of
(TOP-REAL 2) such that A46:
G4 is
open
and A47:
G = G4 /\ ([#] ((TOP-REAL 2) | Qa9))
by A45, TOPS_2:24;
reconsider G5 =
G4 /\ ([#] ((TOP-REAL 2) | (Segment (P,p1,p2,p1,q)))) as
Subset of
((TOP-REAL 2) | (Segment (P,p1,p2,p1,q))) ;
A48:
G5 is
open
by A46, TOPS_2:24;
A49:
rng g1 =
[#] ((TOP-REAL 2) | (Segment (P,p1,p2,p1,q)))
by A37, TOPS_2:def 5
.=
Segment (
P,
p1,
p2,
p1,
q)
by PRE_TOPC:def 5
;
A50:
p1 in Segment (
P,
p1,
p2,
p1,
q)
by A36, TOPREAL1:1;
A51:
f1 " G5 =
g1 " (G4 /\ (Segment (P,p1,p2,p1,q)))
by PRE_TOPC:def 5
.=
(g1 " G4) /\ (g1 " (Segment (P,p1,p2,p1,q)))
by FUNCT_1:68
;
g1 " G =
(g1 " G4) /\ (g1 " ([#] ((TOP-REAL 2) | Qa9)))
by A47, FUNCT_1:68
.=
(g1 " G4) /\ (g1 " Qa9)
by PRE_TOPC:def 5
.=
(g1 " G4) /\ (g1 " ((rng g1) /\ Qa9))
by RELAT_1:133
.=
(g1 " G4) /\ (g1 " (Segment (P,p1,p2,p1,q)))
by A42, A49, XBOOLE_1:28
;
hence
g1 " G is
open
by A43, A50, A48, A51, TOPS_2:43;
verum
end;
[#] (((TOP-REAL 2) | P) | Qa) <> {}
;
then A52:
g1 is
continuous
by A44, TOPS_2:43;
then
p19,
q9 are_connected
by A38, BORSUK_2:def 1;
then
g1 is
Path of
p19,
q9
by A38, A52, BORSUK_2:def 2;
hence
ex
G1 being
Path of
p19,
q9 st
(
G1 is
continuous &
G1 . 0 = p19 &
G1 . 1
= q9 )
by A38, A52;
verum end; then consider G1 being
Path of
p19,
q9 such that A55:
(
G1 is
continuous &
G1 . 0 = p19 &
G1 . 1
= q9 )
;
now ( ( q2 <> p2 & ex G3 being Path of q29,p29 st
( G3 is continuous & G3 . 0 = q29 & G3 . 1 = p29 ) ) or ( q2 = p2 & ex G3 being Path of q29,p29 st
( G3 is continuous & G3 . 0 = q29 & G3 . 1 = p29 ) ) )per cases
( q2 <> p2 or q2 = p2 )
;
case
q2 <> p2
;
ex G3 being Path of q29,p29 st
( G3 is continuous & G3 . 0 = q29 & G3 . 1 = p29 )then A56:
Segment (
P,
p1,
p2,
q2,
p2)
is_an_arc_of q2,
p2
by A1, A7, Th21;
then consider f3 being
Function of
I[01],
((TOP-REAL 2) | (Segment (P,p1,p2,q2,p2))) such that A57:
f3 is
being_homeomorphism
and A58:
(
f3 . 0 = q2 &
f3 . 1
= p2 )
by TOPREAL1:def 1;
A59:
rng f3 =
[#] ((TOP-REAL 2) | (Segment (P,p1,p2,q2,p2)))
by A57, TOPS_2:def 5
.=
Segment (
P,
p1,
p2,
q2,
p2)
by PRE_TOPC:def 5
;
{ p where p is Point of (TOP-REAL 2) : ( LE q2,p,P,p1,p2 & LE p,p2,P,p1,p2 ) } c= Qa
proof
let x be
object ;
TARSKI:def 3 ( not x in { p where p is Point of (TOP-REAL 2) : ( LE q2,p,P,p1,p2 & LE p,p2,P,p1,p2 ) } or x in Qa )
assume
x in { p where p is Point of (TOP-REAL 2) : ( LE q2,p,P,p1,p2 & LE p,p2,P,p1,p2 ) }
;
x in Qa
then A60:
ex
p being
Point of
(TOP-REAL 2) st
(
x = p &
LE q2,
p,
P,
p1,
p2 &
LE p,
p2,
P,
p1,
p2 )
;
then
x <> q1
by A1, A2, A3, JORDAN5C:12, JORDAN6:37;
then A61:
not
x in {q1}
by TARSKI:def 1;
x in P
by A60, JORDAN5C:def 3;
hence
x in Qa
by A61, XBOOLE_0:def 5;
verum
end; then A62:
Segment (
P,
p1,
p2,
q2,
p2)
c= Qa
by JORDAN6:26;
A63:
the
carrier of
(((TOP-REAL 2) | P) | Qa) = Qa
by PRE_TOPC:8;
dom f3 = the
carrier of
I[01]
by A18, A57, TOPS_2:def 5;
then reconsider g3 =
f3 as
Function of
I[01],
(((TOP-REAL 2) | P) | Qa) by A59, A63, A62, FUNCT_2:2;
A64:
f3 is
continuous
by A57, TOPS_2:def 5;
A65:
for
G being
Subset of
(((TOP-REAL 2) | P) | Qa) st
G is
open holds
g3 " G is
open
proof
let G be
Subset of
(((TOP-REAL 2) | P) | Qa);
( G is open implies g3 " G is open )
A66:
((TOP-REAL 2) | P) | Qa = (TOP-REAL 2) | Qa9
by PRE_TOPC:7, XBOOLE_1:36;
assume
G is
open
;
g3 " G is open
then consider G4 being
Subset of
(TOP-REAL 2) such that A67:
G4 is
open
and A68:
G = G4 /\ ([#] ((TOP-REAL 2) | Qa9))
by A66, TOPS_2:24;
reconsider G5 =
G4 /\ ([#] ((TOP-REAL 2) | (Segment (P,p1,p2,q2,p2)))) as
Subset of
((TOP-REAL 2) | (Segment (P,p1,p2,q2,p2))) ;
A69:
G5 is
open
by A67, TOPS_2:24;
A70:
rng g3 =
[#] ((TOP-REAL 2) | (Segment (P,p1,p2,q2,p2)))
by A57, TOPS_2:def 5
.=
Segment (
P,
p1,
p2,
q2,
p2)
by PRE_TOPC:def 5
;
A71:
p2 in Segment (
P,
p1,
p2,
q2,
p2)
by A56, TOPREAL1:1;
A72:
f3 " G5 =
g3 " (G4 /\ (Segment (P,p1,p2,q2,p2)))
by PRE_TOPC:def 5
.=
(g3 " G4) /\ (g3 " (Segment (P,p1,p2,q2,p2)))
by FUNCT_1:68
;
g3 " G =
(g3 " G4) /\ (g3 " ([#] ((TOP-REAL 2) | Qa9)))
by A68, FUNCT_1:68
.=
(g3 " G4) /\ (g3 " Qa9)
by PRE_TOPC:def 5
.=
(g3 " G4) /\ (g3 " ((rng g3) /\ Qa9))
by RELAT_1:133
.=
(g3 " G4) /\ (g3 " (Segment (P,p1,p2,q2,p2)))
by A62, A70, XBOOLE_1:28
;
hence
g3 " G is
open
by A64, A71, A69, A72, TOPS_2:43;
verum
end;
[#] (((TOP-REAL 2) | P) | Qa) <> {}
;
then A73:
g3 is
continuous
by A65, TOPS_2:43;
then
q29,
p29 are_connected
by A58, BORSUK_2:def 1;
then
g3 is
Path of
q29,
p29
by A58, A73, BORSUK_2:def 2;
hence
ex
G3 being
Path of
q29,
p29 st
(
G3 is
continuous &
G3 . 0 = q29 &
G3 . 1
= p29 )
by A58, A73;
verum end; then consider G3 being
Path of
q29,
p29 such that A76:
(
G3 is
continuous &
G3 . 0 = q29 &
G3 . 1
= p29 )
;
{ p where p is Point of (TOP-REAL 2) : ( LE q,p,Q1,q1,q2 & LE p,q2,Q1,q1,q2 ) } c= Qa
proof
let x be
object ;
TARSKI:def 3 ( not x in { p where p is Point of (TOP-REAL 2) : ( LE q,p,Q1,q1,q2 & LE p,q2,Q1,q1,q2 ) } or x in Qa )
assume
x in { p where p is Point of (TOP-REAL 2) : ( LE q,p,Q1,q1,q2 & LE p,q2,Q1,q1,q2 ) }
;
x in Qa
then A77:
ex
p being
Point of
(TOP-REAL 2) st
(
x = p &
LE q,
p,
Q1,
q1,
q2 &
LE p,
q2,
Q1,
q1,
q2 )
;
now not x = q1assume A78:
x = q1
;
contradiction
LE q1,
q,
Q1,
q1,
q2
by A2, A20, JORDAN5C:10;
hence
contradiction
by A2, A22, A77, A78, JORDAN5C:12;
verum end;
then A79:
not
x in {q1}
by TARSKI:def 1;
x in Q1
by A77, JORDAN5C:def 3;
hence
x in Qa
by A4, A79, XBOOLE_0:def 5;
verum
end; then A80:
Segment (
Q1,
q1,
q2,
q,
q2)
c= Qa
by JORDAN6:26;
dom f2 = the
carrier of
I[01]
by A18, A29, TOPS_2:def 5;
then reconsider g2 =
f2 as
Function of
I[01],
(((TOP-REAL 2) | P) | Qa) by A31, A27, A80, FUNCT_2:2;
A81:
f2 is
continuous
by A29, TOPS_2:def 5;
A82:
for
G being
Subset of
(((TOP-REAL 2) | P) | Qa) st
G is
open holds
g2 " G is
open
proof
let G be
Subset of
(((TOP-REAL 2) | P) | Qa);
( G is open implies g2 " G is open )
A83:
((TOP-REAL 2) | P) | Qa = (TOP-REAL 2) | Qa9
by PRE_TOPC:7, XBOOLE_1:36;
assume
G is
open
;
g2 " G is open
then consider G4 being
Subset of
(TOP-REAL 2) such that A84:
G4 is
open
and A85:
G = G4 /\ ([#] ((TOP-REAL 2) | Qa9))
by A83, TOPS_2:24;
reconsider G5 =
G4 /\ ([#] ((TOP-REAL 2) | (Segment (Q1,q1,q2,q,q2)))) as
Subset of
((TOP-REAL 2) | (Segment (Q1,q1,q2,q,q2))) ;
A86:
G5 is
open
by A84, TOPS_2:24;
A87:
rng g2 =
[#] ((TOP-REAL 2) | (Segment (Q1,q1,q2,q,q2)))
by A29, TOPS_2:def 5
.=
Segment (
Q1,
q1,
q2,
q,
q2)
by PRE_TOPC:def 5
;
A88:
q2 in Segment (
Q1,
q1,
q2,
q,
q2)
by A28, TOPREAL1:1;
A89:
f2 " G5 =
g2 " (G4 /\ (Segment (Q1,q1,q2,q,q2)))
by PRE_TOPC:def 5
.=
(g2 " G4) /\ (g2 " (Segment (Q1,q1,q2,q,q2)))
by FUNCT_1:68
;
g2 " G =
(g2 " G4) /\ (g2 " ([#] ((TOP-REAL 2) | Qa9)))
by A85, FUNCT_1:68
.=
(g2 " G4) /\ (g2 " Qa9)
by PRE_TOPC:def 5
.=
(g2 " G4) /\ (g2 " ((rng g2) /\ Qa9))
by RELAT_1:133
.=
(g2 " G4) /\ (g2 " (Segment (Q1,q1,q2,q,q2)))
by A80, A87, XBOOLE_1:28
;
hence
g2 " G is
open
by A81, A88, A86, A89, TOPS_2:43;
verum
end;
[#] (((TOP-REAL 2) | P) | Qa) <> {}
;
then A90:
g2 is
continuous
by A82, TOPS_2:43;
then
q9,
q29 are_connected
by A30, BORSUK_2:def 1;
then reconsider G2 =
g2 as
Path of
q9,
q29 by A30, A90, BORSUK_2:def 2;
A91:
(G1 + G2) . 1
= q29
by A55, A30, A90, BORSUK_2:14;
A92:
(
G1 + G2 is
continuous &
(G1 + G2) . 0 = p19 )
by A55, A30, A90, BORSUK_2:14;
then A93:
((G1 + G2) + G3) . 1
= p29
by A91, A76, BORSUK_2:14;
(
(G1 + G2) + G3 is
continuous &
((G1 + G2) + G3) . 0 = p19 )
by A92, A91, A76, BORSUK_2:14;
hence
contradiction
by A1, A10, A8, A34, A93, Th18;
verum end; case A94:
q in Segment (
P,
p1,
p2,
q2,
p2)
;
contradictionA95:
( not
p1 in {q2} & not
q1 in {q2} )
by A5, A11, TARSKI:def 1;
not
q1 in {q2}
by A5, TARSKI:def 1;
then reconsider Qa =
P \ {q2} as non
empty Subset of
((TOP-REAL 2) | P) by A10, A16, XBOOLE_0:def 5, XBOOLE_1:36;
A96:
the
carrier of
(((TOP-REAL 2) | P) | Qa) = Qa
by PRE_TOPC:8;
reconsider Qa9 =
Qa as
Subset of
(TOP-REAL 2) ;
A97:
the
carrier of
(((TOP-REAL 2) | P) | Qa) = Qa
by PRE_TOPC:8;
A98:
Segment (
Q1,
q1,
q2,
q1,
q)
is_an_arc_of q1,
q
by A2, A20, A22, JORDAN16:24;
then consider f2 being
Function of
I[01],
((TOP-REAL 2) | (Segment (Q1,q1,q2,q1,q))) such that A99:
f2 is
being_homeomorphism
and A100:
(
f2 . 0 = q1 &
f2 . 1
= q )
by TOPREAL1:def 1;
A101:
rng f2 =
[#] ((TOP-REAL 2) | (Segment (Q1,q1,q2,q1,q)))
by A99, TOPS_2:def 5
.=
Segment (
Q1,
q1,
q2,
q1,
q)
by PRE_TOPC:def 5
;
A102:
not
q in {q2}
by A21, A19, TARSKI:def 1;
q in { p3 where p3 is Point of (TOP-REAL 2) : ( LE q2,p3,P,p1,p2 & LE p3,p2,P,p1,p2 ) }
by A94, JORDAN6:26;
then A103:
ex
p3 being
Point of
(TOP-REAL 2) st
(
q = p3 &
LE q2,
p3,
P,
p1,
p2 &
LE p3,
p2,
P,
p1,
p2 )
;
A104:
now not p2 = q2end; then
not
p2 in {q2}
by TARSKI:def 1;
then reconsider p19 =
p1,
q9 =
q,
q19 =
q1,
p29 =
p2 as
Point of
(((TOP-REAL 2) | P) | Qa) by A4, A10, A13, A20, A96, A95, A102, XBOOLE_0:def 5;
now ( ( q <> p2 & ex G1 being Path of q9,p29 st
( G1 is continuous & G1 . 0 = q9 & G1 . 1 = p29 ) ) or ( q = p2 & ex G1 being Path of q9,p29 st
( G1 is continuous & G1 . 0 = q9 & G1 . 1 = p29 ) ) )per cases
( q <> p2 or q = p2 )
;
case
q <> p2
;
ex G1 being Path of q9,p29 st
( G1 is continuous & G1 . 0 = q9 & G1 . 1 = p29 )then A106:
Segment (
P,
p1,
p2,
q,
p2)
is_an_arc_of q,
p2
by A1, A4, A20, Th21;
then consider f1 being
Function of
I[01],
((TOP-REAL 2) | (Segment (P,p1,p2,q,p2))) such that A107:
f1 is
being_homeomorphism
and A108:
(
f1 . 0 = q &
f1 . 1
= p2 )
by TOPREAL1:def 1;
A109:
rng f1 =
[#] ((TOP-REAL 2) | (Segment (P,p1,p2,q,p2)))
by A107, TOPS_2:def 5
.=
Segment (
P,
p1,
p2,
q,
p2)
by PRE_TOPC:def 5
;
{ p where p is Point of (TOP-REAL 2) : ( LE q,p,P,p1,p2 & LE p,p2,P,p1,p2 ) } c= Qa
proof
let x be
object ;
TARSKI:def 3 ( not x in { p where p is Point of (TOP-REAL 2) : ( LE q,p,P,p1,p2 & LE p,p2,P,p1,p2 ) } or x in Qa )
assume
x in { p where p is Point of (TOP-REAL 2) : ( LE q,p,P,p1,p2 & LE p,p2,P,p1,p2 ) }
;
x in Qa
then A110:
ex
p being
Point of
(TOP-REAL 2) st
(
x = p &
LE q,
p,
P,
p1,
p2 &
LE p,
p2,
P,
p1,
p2 )
;
then
x <> q2
by A1, A21, A19, A103, JORDAN5C:12;
then A111:
not
x in {q2}
by TARSKI:def 1;
x in P
by A110, JORDAN5C:def 3;
hence
x in Qa
by A111, XBOOLE_0:def 5;
verum
end; then A112:
Segment (
P,
p1,
p2,
q,
p2)
c= Qa
by JORDAN6:26;
dom f1 = the
carrier of
I[01]
by A18, A107, TOPS_2:def 5;
then reconsider g1 =
f1 as
Function of
I[01],
(((TOP-REAL 2) | P) | Qa) by A96, A109, A112, FUNCT_2:2;
A113:
f1 is
continuous
by A107, TOPS_2:def 5;
A114:
for
G being
Subset of
(((TOP-REAL 2) | P) | Qa) st
G is
open holds
g1 " G is
open
proof
let G be
Subset of
(((TOP-REAL 2) | P) | Qa);
( G is open implies g1 " G is open )
A115:
((TOP-REAL 2) | P) | Qa = (TOP-REAL 2) | Qa9
by PRE_TOPC:7, XBOOLE_1:36;
assume
G is
open
;
g1 " G is open
then consider G4 being
Subset of
(TOP-REAL 2) such that A116:
G4 is
open
and A117:
G = G4 /\ ([#] ((TOP-REAL 2) | Qa9))
by A115, TOPS_2:24;
reconsider G5 =
G4 /\ ([#] ((TOP-REAL 2) | (Segment (P,p1,p2,q,p2)))) as
Subset of
((TOP-REAL 2) | (Segment (P,p1,p2,q,p2))) ;
A118:
G5 is
open
by A116, TOPS_2:24;
A119:
rng g1 =
[#] ((TOP-REAL 2) | (Segment (P,p1,p2,q,p2)))
by A107, TOPS_2:def 5
.=
Segment (
P,
p1,
p2,
q,
p2)
by PRE_TOPC:def 5
;
A120:
p2 in Segment (
P,
p1,
p2,
q,
p2)
by A106, TOPREAL1:1;
A121:
f1 " G5 =
g1 " (G4 /\ (Segment (P,p1,p2,q,p2)))
by PRE_TOPC:def 5
.=
(g1 " G4) /\ (g1 " (Segment (P,p1,p2,q,p2)))
by FUNCT_1:68
;
g1 " G =
(g1 " G4) /\ (g1 " ([#] ((TOP-REAL 2) | Qa9)))
by A117, FUNCT_1:68
.=
(g1 " G4) /\ (g1 " Qa9)
by PRE_TOPC:def 5
.=
(g1 " G4) /\ (g1 " ((rng g1) /\ Qa9))
by RELAT_1:133
.=
(g1 " G4) /\ (g1 " (Segment (P,p1,p2,q,p2)))
by A112, A119, XBOOLE_1:28
;
hence
g1 " G is
open
by A113, A120, A118, A121, TOPS_2:43;
verum
end;
[#] (((TOP-REAL 2) | P) | Qa) <> {}
;
then A122:
g1 is
continuous
by A114, TOPS_2:43;
then
q9,
p29 are_connected
by A108, BORSUK_2:def 1;
then
g1 is
Path of
q9,
p29
by A108, A122, BORSUK_2:def 2;
hence
ex
G1 being
Path of
q9,
p29 st
(
G1 is
continuous &
G1 . 0 = q9 &
G1 . 1
= p29 )
by A108, A122;
verum end; then consider G1 being
Path of
q9,
p29 such that A125:
(
G1 is
continuous &
G1 . 0 = q9 &
G1 . 1
= p29 )
;
now ( ( q1 <> p1 & ex G3 being Path of p19,q19 st
( G3 is continuous & G3 . 0 = p19 & G3 . 1 = q19 ) ) or ( q1 = p1 & ex G3 being Path of p19,q19 st
( G3 is continuous & G3 . 0 = p19 & G3 . 1 = q19 ) ) )per cases
( q1 <> p1 or q1 = p1 )
;
case
q1 <> p1
;
ex G3 being Path of p19,q19 st
( G3 is continuous & G3 . 0 = p19 & G3 . 1 = q19 )then A126:
Segment (
P,
p1,
p2,
p1,
q1)
is_an_arc_of p1,
q1
by A1, A10, JORDAN16:24;
then consider f3 being
Function of
I[01],
((TOP-REAL 2) | (Segment (P,p1,p2,p1,q1))) such that A127:
f3 is
being_homeomorphism
and A128:
(
f3 . 0 = p1 &
f3 . 1
= q1 )
by TOPREAL1:def 1;
A129:
rng f3 =
[#] ((TOP-REAL 2) | (Segment (P,p1,p2,p1,q1)))
by A127, TOPS_2:def 5
.=
Segment (
P,
p1,
p2,
p1,
q1)
by PRE_TOPC:def 5
;
{ p where p is Point of (TOP-REAL 2) : ( LE p1,p,P,p1,p2 & LE p,q1,P,p1,p2 ) } c= Qa
proof
let x be
object ;
TARSKI:def 3 ( not x in { p where p is Point of (TOP-REAL 2) : ( LE p1,p,P,p1,p2 & LE p,q1,P,p1,p2 ) } or x in Qa )
assume
x in { p where p is Point of (TOP-REAL 2) : ( LE p1,p,P,p1,p2 & LE p,q1,P,p1,p2 ) }
;
x in Qa
then A130:
ex
p being
Point of
(TOP-REAL 2) st
(
x = p &
LE p1,
p,
P,
p1,
p2 &
LE p,
q1,
P,
p1,
p2 )
;
then
x <> q2
by A1, A2, A3, JORDAN5C:12, JORDAN6:37;
then A131:
not
x in {q2}
by TARSKI:def 1;
x in P
by A130, JORDAN5C:def 3;
hence
x in Qa
by A131, XBOOLE_0:def 5;
verum
end; then A132:
Segment (
P,
p1,
p2,
p1,
q1)
c= Qa
by JORDAN6:26;
A133:
the
carrier of
(((TOP-REAL 2) | P) | Qa) = Qa
by PRE_TOPC:8;
dom f3 = the
carrier of
I[01]
by A18, A127, TOPS_2:def 5;
then reconsider g3 =
f3 as
Function of
I[01],
(((TOP-REAL 2) | P) | Qa) by A129, A133, A132, FUNCT_2:2;
A134:
f3 is
continuous
by A127, TOPS_2:def 5;
A135:
for
G being
Subset of
(((TOP-REAL 2) | P) | Qa) st
G is
open holds
g3 " G is
open
proof
let G be
Subset of
(((TOP-REAL 2) | P) | Qa);
( G is open implies g3 " G is open )
A136:
((TOP-REAL 2) | P) | Qa = (TOP-REAL 2) | Qa9
by PRE_TOPC:7, XBOOLE_1:36;
assume
G is
open
;
g3 " G is open
then consider G4 being
Subset of
(TOP-REAL 2) such that A137:
G4 is
open
and A138:
G = G4 /\ ([#] ((TOP-REAL 2) | Qa9))
by A136, TOPS_2:24;
reconsider G5 =
G4 /\ ([#] ((TOP-REAL 2) | (Segment (P,p1,p2,p1,q1)))) as
Subset of
((TOP-REAL 2) | (Segment (P,p1,p2,p1,q1))) ;
A139:
G5 is
open
by A137, TOPS_2:24;
A140:
rng g3 =
[#] ((TOP-REAL 2) | (Segment (P,p1,p2,p1,q1)))
by A127, TOPS_2:def 5
.=
Segment (
P,
p1,
p2,
p1,
q1)
by PRE_TOPC:def 5
;
A141:
p1 in Segment (
P,
p1,
p2,
p1,
q1)
by A126, TOPREAL1:1;
A142:
f3 " G5 =
g3 " (G4 /\ (Segment (P,p1,p2,p1,q1)))
by PRE_TOPC:def 5
.=
(g3 " G4) /\ (g3 " (Segment (P,p1,p2,p1,q1)))
by FUNCT_1:68
;
g3 " G =
(g3 " G4) /\ (g3 " ([#] ((TOP-REAL 2) | Qa9)))
by A138, FUNCT_1:68
.=
(g3 " G4) /\ (g3 " Qa9)
by PRE_TOPC:def 5
.=
(g3 " G4) /\ (g3 " ((rng g3) /\ Qa9))
by RELAT_1:133
.=
(g3 " G4) /\ (g3 " (Segment (P,p1,p2,p1,q1)))
by A132, A140, XBOOLE_1:28
;
hence
g3 " G is
open
by A134, A141, A139, A142, TOPS_2:43;
verum
end;
[#] (((TOP-REAL 2) | P) | Qa) <> {}
;
then A143:
g3 is
continuous
by A135, TOPS_2:43;
then
p19,
q19 are_connected
by A128, BORSUK_2:def 1;
then
g3 is
Path of
p19,
q19
by A128, A143, BORSUK_2:def 2;
hence
ex
G3 being
Path of
p19,
q19 st
(
G3 is
continuous &
G3 . 0 = p19 &
G3 . 1
= q19 )
by A128, A143;
verum end; then consider G3 being
Path of
p19,
q19 such that A146:
(
G3 is
continuous &
G3 . 0 = p19 &
G3 . 1
= q19 )
;
{ p where p is Point of (TOP-REAL 2) : ( LE q1,p,Q1,q1,q2 & LE p,q,Q1,q1,q2 ) } c= Qa
proof
let x be
object ;
TARSKI:def 3 ( not x in { p where p is Point of (TOP-REAL 2) : ( LE q1,p,Q1,q1,q2 & LE p,q,Q1,q1,q2 ) } or x in Qa )
assume
x in { p where p is Point of (TOP-REAL 2) : ( LE q1,p,Q1,q1,q2 & LE p,q,Q1,q1,q2 ) }
;
x in Qa
then A147:
ex
p being
Point of
(TOP-REAL 2) st
(
x = p &
LE q1,
p,
Q1,
q1,
q2 &
LE p,
q,
Q1,
q1,
q2 )
;
now not x = q2assume A148:
x = q2
;
contradiction
LE q,
q2,
Q1,
q1,
q2
by A2, A20, JORDAN5C:10;
hence
contradiction
by A2, A21, A19, A147, A148, JORDAN5C:12;
verum end;
then A149:
not
x in {q2}
by TARSKI:def 1;
x in Q1
by A147, JORDAN5C:def 3;
hence
x in Qa
by A4, A149, XBOOLE_0:def 5;
verum
end; then A150:
Segment (
Q1,
q1,
q2,
q1,
q)
c= Qa
by JORDAN6:26;
dom f2 = the
carrier of
I[01]
by A18, A99, TOPS_2:def 5;
then reconsider g2 =
f2 as
Function of
I[01],
(((TOP-REAL 2) | P) | Qa) by A101, A97, A150, FUNCT_2:2;
A151:
f2 is
continuous
by A99, TOPS_2:def 5;
A152:
for
G being
Subset of
(((TOP-REAL 2) | P) | Qa) st
G is
open holds
g2 " G is
open
proof
let G be
Subset of
(((TOP-REAL 2) | P) | Qa);
( G is open implies g2 " G is open )
A153:
((TOP-REAL 2) | P) | Qa = (TOP-REAL 2) | Qa9
by PRE_TOPC:7, XBOOLE_1:36;
assume
G is
open
;
g2 " G is open
then consider G4 being
Subset of
(TOP-REAL 2) such that A154:
G4 is
open
and A155:
G = G4 /\ ([#] ((TOP-REAL 2) | Qa9))
by A153, TOPS_2:24;
reconsider G5 =
G4 /\ ([#] ((TOP-REAL 2) | (Segment (Q1,q1,q2,q1,q)))) as
Subset of
((TOP-REAL 2) | (Segment (Q1,q1,q2,q1,q))) ;
A156:
G5 is
open
by A154, TOPS_2:24;
A157:
rng g2 =
[#] ((TOP-REAL 2) | (Segment (Q1,q1,q2,q1,q)))
by A99, TOPS_2:def 5
.=
Segment (
Q1,
q1,
q2,
q1,
q)
by PRE_TOPC:def 5
;
A158:
q1 in Segment (
Q1,
q1,
q2,
q1,
q)
by A98, TOPREAL1:1;
A159:
f2 " G5 =
g2 " (G4 /\ (Segment (Q1,q1,q2,q1,q)))
by PRE_TOPC:def 5
.=
(g2 " G4) /\ (g2 " (Segment (Q1,q1,q2,q1,q)))
by FUNCT_1:68
;
g2 " G =
(g2 " G4) /\ (g2 " ([#] ((TOP-REAL 2) | Qa9)))
by A155, FUNCT_1:68
.=
(g2 " G4) /\ (g2 " Qa9)
by PRE_TOPC:def 5
.=
(g2 " G4) /\ (g2 " ((rng g2) /\ Qa9))
by RELAT_1:133
.=
(g2 " G4) /\ (g2 " (Segment (Q1,q1,q2,q1,q)))
by A150, A157, XBOOLE_1:28
;
hence
g2 " G is
open
by A151, A158, A156, A159, TOPS_2:43;
verum
end;
[#] (((TOP-REAL 2) | P) | Qa) <> {}
;
then A160:
g2 is
continuous
by A152, TOPS_2:43;
then
q19,
q9 are_connected
by A100, BORSUK_2:def 1;
then reconsider G2 =
g2 as
Path of
q19,
q9 by A100, A160, BORSUK_2:def 2;
A161:
(G2 + G1) . 1
= p29
by A125, A100, A160, BORSUK_2:14;
A162:
(
G2 + G1 is
continuous &
(G2 + G1) . 0 = q19 )
by A125, A100, A160, BORSUK_2:14;
then A163:
(G3 + (G2 + G1)) . 1
= p29
by A161, A146, BORSUK_2:14;
(
G3 + (G2 + G1) is
continuous &
(G3 + (G2 + G1)) . 0 = p19 )
by A162, A161, A146, BORSUK_2:14;
hence
contradiction
by A1, A7, A11, A104, A163, Th18;
verum end; hence
contradiction
;
verum end;
hence
Q1 = Segment (P,p1,p2,q1,q2)
by A2, A6, Th20; verum