let FT be non empty RelStr ; for A being Subset of FT st FT is symmetric holds
( A is connected iff A is arcwise_connected )
let A be Subset of FT; ( FT is symmetric implies ( A is connected iff A is arcwise_connected ) )
assume A1:
FT is symmetric
; ( A is connected iff A is arcwise_connected )
now ( not A is arcwise_connected implies not A is connected )assume
not
A is
arcwise_connected
;
not A is connected then consider x1,
x2 being
Element of
FT such that A2:
x1 in A
and A3:
x2 in A
and A4:
for
f being
FinSequence of
FT holds
( not
f is
continuous or not
rng f c= A or not
f . 1
= x1 or not
f . (len f) = x2 )
;
A5:
{ z where z is Element of FT : ( z in A & ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = z ) ) } c= A
then reconsider G =
{ z where z is Element of FT : ( z in A & ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = z ) ) } as
Subset of
FT by XBOOLE_1:1;
A6:
G misses A \ G
by XBOOLE_1:79;
A7:
now not G ^b meets A \ Gassume
G ^b meets A \ G
;
contradictionthen consider u being
object such that A8:
u in G ^b
and A9:
u in A \ G
by XBOOLE_0:3;
A10:
not
u in G
by A9, XBOOLE_0:def 5;
consider x being
Element of
FT such that A11:
u = x
and A12:
U_FT x meets G
by A8;
consider y being
object such that A13:
y in U_FT x
and A14:
y in G
by A12, XBOOLE_0:3;
consider z2 being
Element of
FT such that A15:
y = z2
and
z2 in A
and A16:
ex
f being
FinSequence of
FT st
(
f is
continuous &
rng f c= A &
f . 1
= x1 &
f . (len f) = z2 )
by A14;
consider f being
FinSequence of
FT such that A17:
f is
continuous
and A18:
rng f c= A
and A19:
f . 1
= x1
and A20:
f . (len f) = z2
by A16;
reconsider g =
f ^ <*x*> as
FinSequence of
FT ;
A21:
rng g =
(rng f) \/ (rng <*x*>)
by FINSEQ_1:31
.=
(rng f) \/ {x}
by FINSEQ_1:38
;
A22:
u in A
by A9, XBOOLE_0:def 5;
then
{x} c= A
by A11, ZFMISC_1:31;
then A23:
rng g c= A
by A18, A21, XBOOLE_1:8;
1
<= len f
by A17;
then
1
in dom f
by FINSEQ_3:25;
then A24:
(
g . ((len f) + 1) = x &
g . 1
= x1 )
by A19, FINSEQ_1:42, FINSEQ_1:def 7;
x in U_FT z2
by A1, A13, A15;
then A25:
g is
continuous
by A17, A20, Th43;
len g =
(len f) + (len <*x*>)
by FINSEQ_1:22
.=
(len f) + 1
by FINSEQ_1:39
;
hence
contradiction
by A22, A10, A11, A25, A24, A23;
verum end;
A = G \/ (A \ G)
by A5, XBOOLE_1:45;
hence
not
A is
connected
by A30, A26, A6, A7;
verum end;
hence
( A is connected implies A is arcwise_connected )
; ( A is arcwise_connected implies A is connected )
now ( not A is connected implies ( not A is arcwise_connected & not A is arcwise_connected ) )assume
not
A is
connected
;
( not A is arcwise_connected & not A is arcwise_connected )then consider P,
Q being
Subset of
FT such that A31:
A = P \/ Q
and A32:
P <> {}
and A33:
Q <> {}
and A34:
P misses Q
and A35:
P ^b misses Q
;
set q0 = the
Element of
Q;
the
Element of
Q in Q
by A33;
then reconsider q1 = the
Element of
Q as
Element of
FT ;
set p0 = the
Element of
P;
the
Element of
P in P
by A32;
then reconsider p1 = the
Element of
P as
Element of
FT ;
A36:
(
p1 in A &
q1 in A )
by A31, A32, A33, XBOOLE_0:def 3;
hereby not A is arcwise_connected
assume
A is
arcwise_connected
;
contradictionthen consider f being
FinSequence of
FT such that A37:
f is
continuous
and A38:
rng f c= A
and A39:
f . 1
= p1
and A40:
f . (len f) = q1
by A36;
defpred S1[
Nat]
means ( 1
<= $1 & $1
<= len f &
f . $1
in P );
len f >= 1
by A37;
then A41:
ex
k being
Nat st
S1[
k]
by A32, A39;
A42:
for
k being
Nat st
S1[
k] holds
k <= len f
;
consider i0 being
Nat such that A43:
(
S1[
i0] & ( for
n being
Nat st
S1[
n] holds
n <= i0 ) )
from NAT_1:sch 6(A42, A41);
i0 <> len f
by A33, A34, A40, A43, XBOOLE_0:3;
then A44:
i0 < len f
by A43, XXREAL_0:1;
then A45:
i0 + 1
<= len f
by NAT_1:13;
reconsider u0 =
f . i0 as
Element of
FT by A43;
A46:
1
< i0 + 1
by A43, NAT_1:13;
then
i0 + 1
in dom f
by A45, FINSEQ_3:25;
then A47:
f . (i0 + 1) in rng f
by FUNCT_1:def 3;
then reconsider z0 =
f . (i0 + 1) as
Element of
FT ;
z0 in U_FT u0
by A37, A43, A44;
then
f . i0 in U_FT z0
by A1;
then
U_FT z0 meets P
by A43, XBOOLE_0:3;
then A48:
z0 in P ^b
;
then
f . (i0 + 1) in Q
by A31, A38, A47, XBOOLE_0:def 3;
hence
contradiction
by A35, A48, XBOOLE_0:3;
verum
end; hence
not
A is
arcwise_connected
;
verum end;
hence
( A is arcwise_connected implies A is connected )
; verum