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 H₁( 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= H₁(B) & H₁(B) c= A )

proof

let B be Subset of FT; :: thesis: ( B c= A implies ( B c= H₁(B) & H₁(B) c= A ) )
assume A4: B c= A ; :: thesis: ( B c= H₁(B) & H₁(B) c= A )
B c= B ^b by Th13;
hence B c= (B ^b) /\ A by A4, XBOOLE_1:19; :: thesis: H₁(B) c= A
thus H₁(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) = H₁(S /. i) and
A9: H₁(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 A6, NAT_1:6;
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 S₁[ Nat] means ( $1 < len S implies S /. ($1 + 1) <> {} );

A13: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A14: S₁[i] ; :: thesis: S₁[i + 1]
thus S₁[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 A14, A15, NAT_1:13; :: thesis: verum

end;

end;

A16: S₁[ 0 ] by A7;
A17: for i being Nat holds S₁[i] from NAT_1:sch 2(A16, A13);
reconsider k = k as Element of NAT by ORDINAL1:def 12;
k < len S by A11, NAT_1:13;
then A18: S /. (len S) <> {} by A17, A11;
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 XBOOLE_1:28, XBOOLE_1:36
.= (S /. (len S)) /\ (A \ (S /. (len S))) by A9, XBOOLE_1:16
.= {} 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 A9, XBOOLE_1:12, XBOOLE_1:17 ;
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 A22, A23, XBOOLE_0:def 3;
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 A27, NAT_1:6;
defpred S₁[ 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 A22, XBOOLE_1:23
.= B by Th13, XBOOLE_1:28 ;

A33: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A34: S₁[i] ; :: thesis: S₁[i + 1]
thus S₁[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 A34, Th14, NAT_1:13;
then ((S /. (i + 1)) ^b) /\ A c= (B ^b) /\ A by XBOOLE_1:26;
hence S /. ((i + 1) + 1) c= B by A32, A29, A35; :: thesis: verum

end;

end;

A36: S₁[ 0 ] by A23, A28, ZFMISC_1:31;
A37: for i being Nat holds S₁[i] from NAT_1:sch 2(A36, A33);
reconsider k = k as Element of NAT by ORDINAL1:def 12;
k < len S by A31, NAT_1:13;
then A38: S /. (len S) c= B by A37, A31;
A39: B c= A by A22, XBOOLE_1:7;
then S /. (len S) c= A by A38;
then S /. (len S) = A by A30;
then A40: A = B by A39, A38;
B /\ C = {} by A25;
hence contradiction by A22, A24, A40, XBOOLE_1:7, XBOOLE_1:28; :: thesis: verum