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 )
now :: thesis: ( not A is arcwise_connected implies not 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
proof
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;
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 :: 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 ;
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 ;
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) \/ () by FINSEQ_1:31
.= (rng f) \/ {x} by FINSEQ_1:38 ;
A22: u in A by ;
then {x} c= A by ;
then A23: rng g c= A by ;
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 ;
x in U_FT z2 by A1, A13, A15;
then A25: g is continuous by ;
len g = (len f) + () by FINSEQ_1:22
.= (len f) + 1 by FINSEQ_1:39 ;
hence contradiction by A22, A10, A11, A25, A24, A23; :: thesis: verum
end;
A26: now :: thesis: not G = {} end;
A30: now :: thesis: not A \ G = {}
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;
A = G \/ (A \ G) by ;
hence not A is connected by A30, A26, A6, A7; :: thesis: verum
end;
hence ( A is connected implies A is arcwise_connected ) ; :: thesis: ( A is arcwise_connected implies A is connected )
now :: thesis: ( not A is connected implies ( not A is arcwise_connected & not A is arcwise_connected ) )
assume 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 ;
hereby :: thesis: not A is arcwise_connected
assume 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 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 ;
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 i0 <> len f by ;
then A44: i0 < len f by ;
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 ;
then i0 + 1 in dom f by ;
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 ;
then f . i0 in U_FT z0 by A1;
then U_FT z0 meets P by ;
then A48: z0 in P ^b ;
now :: thesis: not f . (i0 + 1) in P
assume f . (i0 + 1) in P ; :: thesis: contradiction
then i0 + 1 <= i0 by ;
hence contradiction by NAT_1:13; :: thesis: verum
end;
then f . (i0 + 1) in Q by ;
hence contradiction by A35, A48, XBOOLE_0:3; :: thesis: verum
end;
hence not A is arcwise_connected ; :: thesis: verum
end;
hence ( A is arcwise_connected implies A is connected ) ; :: thesis: verum