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 )

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_{1}[ 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 ;

_{1}[ 0 ]
by A23, A28, ZFMISC_1:31;

A37: for i being Nat holds S_{1}[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

( 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

assume A21:
for x being Element of FT st x in A holds
deffunc H_{1}( 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_{1}(B) & H_{1}(B) c= A )

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_{1}(S /. i)
and

A9: H_{1}(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_{1}[ Nat] means ( $1 < len S implies S /. ($1 + 1) <> {} );

_{1}[ 0 ]
by A7;

A17: for i being Nat holds S_{1}[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 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

proof

A5:
A is finite
;
let B be Subset of FT; :: thesis: ( B c= A implies ( B c= H_{1}(B) & H_{1}(B) c= A ) )

assume A4: B c= A ; :: thesis: ( B c= H_{1}(B) & H_{1}(B) c= A )

B c= B ^b by Th13;

hence B c= (B ^b) /\ A by A4, XBOOLE_1:19; :: thesis: H_{1}(B) c= A

thus H_{1}(B) c= A
by XBOOLE_1:17; :: thesis: verum

end;assume A4: B c= A ; :: thesis: ( B c= H

B c= B ^b by Th13;

hence B c= (B ^b) /\ A by A4, XBOOLE_1:19; :: thesis: H

thus H

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

A9: H

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

A13: now :: thesis: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]

A16:
SS

let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A14: S_{1}[i]
; :: thesis: S_{1}[i + 1]

thus S_{1}[i + 1]
:: thesis: verum

end;assume A14: S

thus S

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

A17: for i being Nat holds S

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

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

(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_{1}[i] holds

S_{1}[i + 1]

A36:
SS

let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A34: S_{1}[i]
; :: thesis: S_{1}[i + 1]

thus S_{1}[i + 1]
:: thesis: verum

end;assume A34: S

thus S

A37: for i being Nat holds S

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