let FT be non empty finite filled RelStr ; :: thesis: for A being Subset of FT holds
( A is connected iff for x being Element of FT st x in A holds
ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) ) )

let A be Subset of FT; :: thesis: ( A is connected iff for x being Element of FT st x in A holds
ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) ) )

thus ( A is connected implies for x being Element of FT st x in A holds
ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) ) ) :: thesis: ( ( for x being Element of FT st x in A holds
ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) ) ) implies A is connected )
proof
deffunc H1( Subset of FT) -> Element of K32( the carrier of FT) = (\$1 ^b) /\ A;
assume A1: A is connected ; :: thesis: for x being Element of FT st x in A holds
ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) )

let x be Element of FT; :: thesis: ( x in A implies ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) ) )

assume x in A ; :: thesis: ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) )

then A2: {x} c= A by ZFMISC_1:31;
A3: for B being Subset of FT st B c= A holds
( B c= H1(B) & H1(B) c= A )
proof
let B be Subset of FT; :: thesis: ( B c= A implies ( B c= H1(B) & H1(B) c= A ) )
assume A4: B c= A ; :: thesis: ( B c= H1(B) & H1(B) c= A )
B c= B ^b by Th13;
hence B c= (B ^b) /\ A by ; :: thesis: H1(B) c= A
thus H1(B) c= A by XBOOLE_1:17; :: thesis: verum
end;
A5: A is finite ;
consider S being FinSequence of bool the carrier of FT such that
A6: len S > 0 and
A7: S /. 1 = {x} and
A8: for i being Nat st i > 0 & i < len S holds
S /. (i + 1) = H1(S /. i) and
A9: H1(S /. (len S)) = S /. (len S) and
A10: for i, j being Nat st i > 0 & i < j & j <= len S holds
( S /. i c= A & S /. i c< S /. j ) from FIN_TOPO:sch 1(A5, A2, A3);
consider k being Nat such that
A11: len S = k + 1 by ;
set B = S /. (len S);
set C = A \ (S /. (len S));
A12: S /. (len S) misses A \ (S /. (len S)) by XBOOLE_1:79;
defpred S1[ Nat] means ( \$1 < len S implies S /. (\$1 + 1) <> {} );
A13: now :: thesis: for i being Nat st S1[i] holds
S1[i + 1]
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A14: S1[i] ; :: thesis: S1[i + 1]
thus S1[i + 1] :: thesis: verum
proof
assume A15: i + 1 < len S ; :: thesis: S /. ((i + 1) + 1) <> {}
then ( i + 1 < (i + 1) + 1 & (i + 1) + 1 <= len S ) by NAT_1:13;
then S /. (i + 1) c< S /. ((i + 1) + 1) by A10;
then S /. (i + 1) c= S /. ((i + 1) + 1) ;
hence S /. ((i + 1) + 1) <> {} by ; :: thesis: verum
end;
end;
A16: S1[ 0 ] by A7;
A17: for i being Nat holds S1[i] from reconsider k = k as Element of NAT by ORDINAL1:def 12;
k < len S by ;
then A18: S /. (len S) <> {} by ;
take S ; :: thesis: ( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) )

thus len S > 0 by A6; :: thesis: ( S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) )

thus S /. 1 = {x} by A7; :: thesis: ( ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) )

thus for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A by A8; :: thesis: A c= S /. (len S)
assume not A c= S /. (len S) ; :: thesis: contradiction
then A19: A \ (S /. (len S)) <> {} by XBOOLE_1:37;
((S /. (len S)) ^b) /\ (A \ (S /. (len S))) = ((S /. (len S)) ^b) /\ (A /\ (A \ (S /. (len S)))) by
.= (S /. (len S)) /\ (A \ (S /. (len S))) by
.= {} by A12 ;
then A20: ( S /. (len S) misses A \ (S /. (len S)) & (S /. (len S)) ^b misses A \ (S /. (len S)) ) by XBOOLE_1:79;
(S /. (len S)) \/ (A \ (S /. (len S))) = (S /. (len S)) \/ A by XBOOLE_1:39
.= A by ;
hence contradiction by A1, A19, A18, A20; :: thesis: verum
end;
assume A21: for x being Element of FT st x in A holds
ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) ) ; :: thesis: A is connected
given B, C being Subset of FT such that A22: A = B \/ C and
A23: B <> {} and
A24: C <> {} and
A25: B misses C and
A26: B ^b misses C ; :: according to FIN_TOPO:def 16 :: thesis: contradiction
set x = the Element of B;
the Element of B in A by ;
then consider S being FinSequence of bool the carrier of FT such that
A27: len S > 0 and
A28: S /. 1 = { the Element of B} and
A29: for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A and
A30: A c= S /. (len S) by A21;
consider k being Nat such that
A31: len S = k + 1 by ;
defpred S1[ Nat] means ( \$1 < len S implies S /. (\$1 + 1) c= B );
(B ^b) /\ C = {} by A26;
then A32: (B ^b) /\ A = ((B ^b) /\ B) \/ {} by
.= B by ;
A33: now :: thesis: for i being Nat st S1[i] holds
S1[i + 1]
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A34: S1[i] ; :: thesis: S1[i + 1]
thus S1[i + 1] :: thesis: verum
proof
assume A35: i + 1 < len S ; :: thesis: S /. ((i + 1) + 1) c= B
then (S /. (i + 1)) ^b c= B ^b by ;
then ((S /. (i + 1)) ^b) /\ A c= (B ^b) /\ A by XBOOLE_1:26;
hence S /. ((i + 1) + 1) c= B by ; :: thesis: verum
end;
end;
A36: S1[ 0 ] by ;
A37: for i being Nat holds S1[i] from reconsider k = k as Element of NAT by ORDINAL1:def 12;
k < len S by ;
then A38: S /. (len S) c= B by ;
A39: B c= A by ;
then S /. (len S) c= A by A38;
then S /. (len S) = A by A30;
then A40: A = B by ;
B /\ C = {} by A25;
hence contradiction by A22, A24, A40, XBOOLE_1:7, XBOOLE_1:28; :: thesis: verum