let FT be non empty finite filled RelStr ; :: thesis:
let A be Subset of FT; :: thesis:
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:

assume A1: A is connected ; :: thesis:
let x be Element of FT; :: thesis:
assume A2: x in A ; :: thesis:
deffunc H₁( Subset of FT) -> Element of bool the carrier of FT = ($1 ^b ) /\ A;
A3: A is finite ;
A4: {x} c= A by A2, ZFMISC_1:37;
A5: for B being Subset of FT st B c= A holds
( B c= H₁(B) & H₁(B) c= A )

let B be Subset of FT; :: thesis:
assume A6: B c= A ; :: thesis:
B c= B ^b by Th18;
hence B c= (B ^b ) /\ A by A6, XBOOLE_1:19; :: thesis:
thus (B ^b ) /\ A c= A by XBOOLE_1:17; :: thesis:

end;

consider S being FinSequence of bool the carrier of FT such that
A7: len S > 0 and
A8: S /. 1 = {x} and
A9: for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = H₁(S /. i) and
A10: H₁(S /. (len S)) = S /. (len S) and
A11: for i, j being Element of NAT st i > 0 & i < j & j <= len S holds
( S /. i c= A & S /. i c< S /. j ) from FIN_TOPO:sch 1(A3, A4, A5);
take S ; :: thesis:
thus len S > 0 by A7; :: thesis:
thus S /. 1 = {x} by A8; :: thesis:
thus for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b ) /\ A by A9; :: thesis:
set B = S /. (len S);
set C = A \ (S /. (len S));
A12: (S /. (len S)) \/ (A \ (S /. (len S))) = (S /. (len S)) \/ A by XBOOLE_1:39
.= A by A10, XBOOLE_1:12, XBOOLE_1:17 ;
assume not A c= S /. (len S) ; :: thesis:
then A13: A \ (S /. (len S)) <> {} by XBOOLE_1:37;
defpred S₁[ Element of NAT ] means ( $1 < len S implies S /. ($1 + 1) <> {} );
A14: S₁[ 0 ] by A8;

A15: now

let i be Element of NAT ; :: thesis:
assume A16: S₁[i] ; :: thesis:
thus S₁[i + 1] :: thesis:

assume A17: i + 1 < len S ; :: thesis:
A18: i + 1 < (i + 1) + 1 by NAT_1:13;
(i + 1) + 1 <= len S by A17, NAT_1:13;
then S /. (i + 1) c< S /. ((i + 1) + 1) by A11, A18;
then S /. (i + 1) c= S /. ((i + 1) + 1) by XBOOLE_0:def 8;
hence S /. ((i + 1) + 1) <> {} by A16, A17, NAT_1:13; :: thesis:

end;

A19: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A14, A15);
consider k being Nat such that
A20: len S = k + 1 by A7, NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
k < len S by A20, NAT_1:13;
then A21: S /. (len S) <> {} by A19, A20;
A22: S /. (len S) misses A \ (S /. (len S)) by XBOOLE_1:79;
A23: S /. (len S) misses A \ (S /. (len S)) by XBOOLE_1:79;
((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 A10, XBOOLE_1:16
.= {} by A23, XBOOLE_0:def 7 ;
then (S /. (len S)) ^b misses A \ (S /. (len S)) by XBOOLE_0:def 7;
hence contradiction by A1, A12, A13, A21, A22, Def18; :: thesis:

end;

assume A24: 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:
given B, C being Subset of FT such that A25: A = B \/ C and
A26: B <> {} and
A27: C <> {} and
A28: B misses C and
A29: B ^b misses C ; :: according to FIN_TOPO:def 18 :: thesis:
A30: (B ^b ) /\ C = {} by A29, XBOOLE_0:def 7;
A31: B /\ C = {} by A28, XBOOLE_0:def 7;
A32: (B ^b ) /\ A = ((B ^b ) /\ B) \/ {} by A25, A30, XBOOLE_1:23
.= B by Th18, XBOOLE_1:28 ;
consider x being Element of B;
x in A by A25, A26, XBOOLE_0:def 3;
then consider S being FinSequence of bool the carrier of FT such that
A33: len S > 0 and
A34: S /. 1 = {x} and
A35: for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b ) /\ A and
A36: A c= S /. (len S) by A24;
A37: B c= A by A25, XBOOLE_1:7;
defpred S₁[ Element of NAT ] means ( $1 < len S implies S /. ($1 + 1) c= B );
A38: S₁[ 0 ] by A26, A34, ZFMISC_1:37;

A39: now

let i be Element of NAT ; :: thesis:
assume A40: S₁[i] ; :: thesis:
thus S₁[i + 1] :: thesis:

assume A41: i + 1 < len S ; :: thesis:
then (S /. (i + 1)) ^b c= B ^b by A40, Th19, 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, A35, A41; :: thesis:

end;

A42: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A38, A39);
consider k being Nat such that
A43: len S = k + 1 by A33, NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
k < len S by A43, NAT_1:13;
then A44: S /. (len S) c= B by A42, A43;
then S /. (len S) c= A by A37, XBOOLE_1:1;
then S /. (len S) = A by A36, XBOOLE_0:def 10;
then A = B by A37, A44, XBOOLE_0:def 10;
hence contradiction by A25, A27, A31, XBOOLE_1:7, XBOOLE_1:28; :: thesis: