let FT be non empty RelStr ; :: thesis: 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; :: thesis: ( FT is symmetric implies ( A is connected iff A is arcwise_connected ) )

assume A1: FT is symmetric ; :: thesis: ( A is connected iff A is arcwise_connected )

( A is connected iff A is arcwise_connected )

let A be Subset of FT; :: thesis: ( FT is symmetric implies ( A is connected iff A is arcwise_connected ) )

assume A1: FT is symmetric ; :: thesis: ( A is connected iff A is arcwise_connected )

now :: thesis: ( not A is arcwise_connected implies not A is connected )

hence
( A is connected implies A is arcwise_connected )
; :: thesis: ( A is arcwise_connected implies A is connected )assume
not A is arcwise_connected
; :: thesis: 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

( 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;

hence not A is connected by A30, A26, A6, A7; :: thesis: verum

end;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

proof

then reconsider G = { z where z is Element of FT : ( z in A & ex f being FinSequence of FT st
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { 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 ) ) } or x in A )

assume x in { 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 ) ) } ; :: thesis: x in A

then ex z being Element of FT st

( x = z & z in A & ex f being FinSequence of FT st

( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = z ) ) ;

hence x in A ; :: thesis: verum

end;( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = z ) ) } or x in A )

assume x in { 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 ) ) } ; :: thesis: x in A

then ex z being Element of FT st

( x = z & z in A & ex f being FinSequence of FT st

( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = z ) ) ;

hence x in A ; :: thesis: verum

( 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 :: thesis: not G ^b meets A \ G

assume
G ^b meets A \ G
; :: thesis: contradiction

then 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; :: thesis: verum

end;then 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; :: thesis: verum

A26: now :: thesis: not G = {}

{x1} c= A
by A2, ZFMISC_1:31;

then A27: rng <*x1*> c= A by FINSEQ_1:38;

assume A28: G = {} ; :: thesis: contradiction

A29: <*x1*> . 1 = x1 by FINSEQ_1:40;

then <*x1*> . (len <*x1*>) = x1 by FINSEQ_1:39;

then x1 in G by A2, A27, A29;

hence contradiction by A28; :: thesis: verum

end;then A27: rng <*x1*> c= A by FINSEQ_1:38;

assume A28: G = {} ; :: thesis: contradiction

A29: <*x1*> . 1 = x1 by FINSEQ_1:40;

then <*x1*> . (len <*x1*>) = x1 by FINSEQ_1:39;

then x1 in G by A2, A27, A29;

hence contradiction by A28; :: thesis: verum

A30: now :: thesis: not A \ G = {}

A = G \/ (A \ G)
by A5, XBOOLE_1:45;assume
A \ G = {}
; :: thesis: contradiction

then A c= G by XBOOLE_1:37;

then G = A by A5;

then ex z being Element of FT st

( z = x2 & z in A & ex f being FinSequence of FT st

( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = z ) ) by A3;

hence contradiction by A4; :: thesis: verum

end;then A c= G by XBOOLE_1:37;

then G = A by A5;

then ex z being Element of FT st

( z = x2 & z in A & ex f being FinSequence of FT st

( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = z ) ) by A3;

hence contradiction by A4; :: thesis: verum

hence not A is connected by A30, A26, A6, A7; :: thesis: verum

now :: thesis: ( not A is connected implies ( not A is arcwise_connected & not A is arcwise_connected ) )

hence
( A is arcwise_connected implies A is connected )
; :: thesis: verumassume
not A is connected
; :: thesis: ( 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;

end;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 :: thesis: not A is arcwise_connected

hence
not A is arcwise_connected
; :: thesis: verumassume
A is arcwise_connected
; :: thesis: contradiction

then 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 S_{1}[ Nat] means ( 1 <= $1 & $1 <= len f & f . $1 in P );

len f >= 1 by A37;

then A41: ex k being Nat st S_{1}[k]
by A32, A39;

A42: for k being Nat st S_{1}[k] holds

k <= len f ;

consider i0 being Nat such that

A43: ( S_{1}[i0] & ( for n being Nat st S_{1}[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 ;

hence contradiction by A35, A48, XBOOLE_0:3; :: thesis: verum

end;then 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 S

len f >= 1 by A37;

then A41: ex k being Nat st S

A42: for k being Nat st S

k <= len f ;

consider i0 being Nat such that

A43: ( S

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 ;

now :: thesis: not f . (i0 + 1) in P

then
f . (i0 + 1) in Q
by A31, A38, A47, XBOOLE_0:def 3;assume
f . (i0 + 1) in P
; :: thesis: contradiction

then i0 + 1 <= i0 by A43, A45, A46;

hence contradiction by NAT_1:13; :: thesis: verum

end;then i0 + 1 <= i0 by A43, A45, A46;

hence contradiction by NAT_1:13; :: thesis: verum

hence contradiction by A35, A48, XBOOLE_0:3; :: thesis: verum