let S be non empty non void identifying_close_blocks without_isolated_points TopStruct ; :: thesis: ( S is strongly_connected implies S is connected )
assume A1: S is strongly_connected ; :: thesis: S is connected
thus S is connected :: thesis: verum
proof
let x, y be Point of S; :: according to PENCIL_1:def 10 :: thesis: ex f being FinSequence of the carrier of S st
( x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
for a, b being Point of S st a = f . i & b = f . (i + 1) holds
a,b are_collinear ) )
A2: len <*x*> = 1 by FINSEQ_1:39;
A3: len <*y*> = 1 by FINSEQ_1:39;
consider K being Block of S such that
A4: x in K by Def9;
K in the topology of S ;
then reconsider L = K as Subset of S ;
( L is closed_under_lines & L is strong ) by Th20, Th21;
then consider f being FinSequence of bool the carrier of S such that
A5: L = f . 1 and
A6: y in f . (len f) and
A7: for W being Subset of S st W in rng f holds
( W is closed_under_lines & W is strong ) and
A8: for i being Nat st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) by A1;
A9: len f in dom f by A6, FUNCT_1:def 2;
A10: 1 in dom f by A4, A5, FUNCT_1:def 2;
then reconsider n = (len f) - 1 as Nat by FINSEQ_3:26;
deffunc H1( Nat) -> set = (f . $1) /\ (f . ($1 + 1));
reconsider n = n as Element of NAT by ORDINAL1:def 12;
consider h being FinSequence such that
A11: ( len h = n & ( for k being Nat st k in dom h holds
h . k = H1(k) ) ) from FINSEQ_1:sch 2();
 A12: dom h = Seg n by A11, FINSEQ_1:def 3;
A13: (len h) + 1 = len f by A11;
now :: thesis: not {} in rng h
assume {} in rng h ; :: thesis: contradiction
then consider i being object such that
A14: i in dom h and
A15: h . i = {} by FUNCT_1:def 3;
reconsider i = i as Element of NAT by A14;
A16: i <= len h by A14, FINSEQ_3:25;
then A17: i < len f by A13, NAT_1:13;
A18: 1 <= i by A14, FINSEQ_3:25;
then i in Seg n by A11, A16, FINSEQ_1:1;
then h . i = (f . i) /\ (f . (i + 1)) by A11, A12;
then 2 c= card (h . i) by A8, A18, A17;
hence contradiction by A15; :: thesis: verum
end;
then product h <> {} by CARD_3:26;
then consider c being object such that
A19: c in product h by XBOOLE_0:def 1;
A20: ex ce being Function st
( ce = c & dom ce = dom h & ( for a being object st a in dom h holds
ce . a in h . a ) ) by A19, CARD_3:def 5;
then reconsider c = c as Function ;
A21: dom h = Seg n by A11, FINSEQ_1:def 3;
then reconsider c = c as FinSequence by A20, FINSEQ_1:def 2;
A22: rng f c= bool the carrier of S by FINSEQ_1:def 4;
rng ((<*x*> ^ c) ^ <*y*>) c= the carrier of S
proof
let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in rng ((<*x*> ^ c) ^ <*y*>) or r in the carrier of S )
assume r in rng ((<*x*> ^ c) ^ <*y*>) ; :: thesis: r in the carrier of S
then r in (rng (<*x*> ^ c)) \/ (rng <*y*>) by FINSEQ_1:31;
then ( r in rng (<*x*> ^ c) or r in rng <*y*> ) by XBOOLE_0:def 3;
then A23: ( r in (rng <*x*>) \/ (rng c) or r in rng <*y*> ) by FINSEQ_1:31;
per cases ( r in rng <*x*> or r in rng c or r in rng <*y*> ) by A23, XBOOLE_0:def 3;
suppose r in rng c ; :: thesis: r in the carrier of S
then consider o being object such that
A24: o in dom c and
A25: r = c . o by FUNCT_1:def 3;
reconsider o = o as Element of NAT by A24;
h . o = (f . o) /\ (f . (o + 1)) by A11, A20, A24;
then r in (f . o) /\ (f . (o + 1)) by A20, A24, A25;
then A26: r in f . o by XBOOLE_0:def 4;
len h <= len f by A13, NAT_1:11;
then dom h c= dom f by FINSEQ_3:30;
then f . o in rng f by A20, A24, FUNCT_1:def 3;
hence r in the carrier of S by A22, A26; :: thesis: verum
end;
end;
end;
then reconsider g = (<*x*> ^ c) ^ <*y*> as FinSequence of the carrier of S by FINSEQ_1:def 4;
A27: len (<*x*> ^ c) = (len <*x*>) + (len c) by FINSEQ_1:22;
then A28: len (<*x*> ^ c) = (len c) + 1 by FINSEQ_1:39;
take g ; :: thesis: ( x = g . 1 & y = g . (len g) & ( for i being Nat st 1 <= i & i < len g holds
for a, b being Point of S st a = g . i & b = g . (i + 1) holds
a,b are_collinear ) )
A29: g = <*x*> ^ (c ^ <*y*>) by FINSEQ_1:32;
hence x = g . 1 by FINSEQ_1:41; :: thesis: ( y = g . (len g) & ( for i being Nat st 1 <= i & i < len g holds
for a, b being Point of S st a = g . i & b = g . (i + 1) holds
a,b are_collinear ) )
len g = (len (<*x*> ^ c)) + (len <*y*>) by FINSEQ_1:22;
then A30: (len (<*x*> ^ c)) + 1 = len g by FINSEQ_1:39;
hence A31: y = g . (len g) by FINSEQ_1:42; :: thesis: for i being Nat st 1 <= i & i < len g holds
for a, b being Point of S st a = g . i & b = g . (i + 1) holds
a,b are_collinear
let i be Nat; :: thesis: ( 1 <= i & i < len g implies for a, b being Point of S st a = g . i & b = g . (i + 1) holds
a,b are_collinear )
assume that
A32: 1 <= i and
A33: i < len g ; :: thesis: for a, b being Point of S st a = g . i & b = g . (i + 1) holds
a,b are_collinear
A34: i <= len (<*x*> ^ c) by A30, A33, NAT_1:13;
let a, b be Point of S; :: thesis: ( a = g . i & b = g . (i + 1) implies a,b are_collinear )
assume that
A35: a = g . i and
A36: b = g . (i + 1) ; :: thesis: a,b are_collinear
reconsider i = i as Element of NAT by ORDINAL1:def 12;
per cases ( ( i = 1 & i <= len c ) or ( i = 1 & i = (len c) + 1 ) or ( 1 < i & i <= len c ) or ( 1 < i & i = (len c) + 1 ) ) by A28, A32, A34, NAT_1:8, XXREAL_0:1;
suppose A37: ( i = 1 & i <= len c ) ; :: thesis: a,b are_collinear
( len (c ^ <*y*>) = (len c) + 1 & len (<*x*> ^ (c ^ <*y*>)) = (len <*x*>) + (len (c ^ <*y*>)) ) by A3, FINSEQ_1:22;
then A38: len (<*x*> ^ (c ^ <*y*>)) = (1 + 1) + (len c) by A2;
A39: 1 in dom c by A37, FINSEQ_3:25;
b = (<*x*> ^ (c ^ <*y*>)) . 2 by A36, A37, FINSEQ_1:32;
then b = (c ^ <*y*>) . (2 - (len <*x*>)) by A2, A38, FINSEQ_1:24, NAT_1:11;
then b = (c ^ <*y*>) . (2 - 1) by FINSEQ_1:39;
then A40: b = c . 1 by A39, FINSEQ_1:def 7;
( c . 1 in h . 1 & h . 1 = (f . 1) /\ (f . (1 + 1)) ) by A11, A20, A39;
then A41: b in f . 1 by A40, XBOOLE_0:def 4;
A42: f . 1 in rng f by A10, FUNCT_1:def 3;
then reconsider f1 = f . 1 as Subset of S by A22;
A43: ( f1 is closed_under_lines & f1 is strong ) by A7, A42;
a = x by A29, A35, A37, FINSEQ_1:41;
hence a,b are_collinear by A4, A5, A41, A43; :: thesis: verum
end;
suppose A48: ( 1 < i & i <= len c ) ; :: thesis: a,b are_collinear
A49: ( len h <= (len h) + 1 & len c = len h ) by A20, FINSEQ_3:29, NAT_1:11;
then i <= (len h) + 1 by A48, XXREAL_0:2;
then A50: i in dom f by A11, A48, FINSEQ_3:25;
then reconsider j = i - 1 as Nat by FINSEQ_3:26;
i <= (len c) + 1 by A48, A49, XXREAL_0:2;
then i in dom (<*x*> ^ c) by A28, A48, FINSEQ_3:25;
then A51: a = (<*x*> ^ c) . i by A35, FINSEQ_1:def 7;
i <= len (<*x*> ^ c) by A27, A2, A48, NAT_1:13;
then A52: a = c . j by A2, A48, A51, FINSEQ_1:24;
j + 1 = i ;
then A53: 1 <= j by A48, NAT_1:13;
A54: f . i in rng f by A50, FUNCT_1:def 3;
then reconsider ff = f . i as Subset of S by A22;
A55: j <= j + 1 by NAT_1:11;
A56: ( len <*x*> < i + 1 & i + 1 <= (len c) + 1 ) by A2, A48, NAT_1:13, XREAL_1:6;
then i + 1 in dom (<*x*> ^ c) by A27, A2, FINSEQ_3:25;
then b = (<*x*> ^ c) . (i + 1) by A36, FINSEQ_1:def 7;
then A57: b = c . ((i + 1) - (len <*x*>)) by A28, A56, FINSEQ_1:24;
i <= len h by A20, A48, FINSEQ_3:29;
then A58: i in Seg n by A11, A48, FINSEQ_1:1;
then c . i in h . i by A20, A21;
then b in (f . i) /\ (f . (i + 1)) by A11, A12, A2, A58, A57;
then A59: b in ff by XBOOLE_0:def 4;
i <= len h by A20, A48, FINSEQ_3:29;
then j <= n by A11, A55, XXREAL_0:2;
then A60: j in Seg n by A53, FINSEQ_1:1;
then c . j in h . j by A20, A21;
then a in (f . j) /\ (f . (j + 1)) by A11, A12, A60, A52;
then A61: a in ff by XBOOLE_0:def 4;
( ff is closed_under_lines & ff is strong ) by A7, A54;
hence a,b are_collinear by A61, A59; :: thesis: verum
end;
suppose A62: ( 1 < i & i = (len c) + 1 ) ; :: thesis: a,b are_collinear
then 0 + 1 < (len c) + 1 ;
then ex k being Nat st len c = k + 1 by NAT_1:6;
then 1 <= len c by NAT_1:11;
then A63: len c in dom h by A20, FINSEQ_3:25;
A64: len (<*x*> ^ c) = 1 + (len c) by A2, FINSEQ_1:22;
then i in dom (<*x*> ^ c) by A62, FINSEQ_3:25;
then a = (<*x*> ^ c) . i by A35, FINSEQ_1:def 7
.= c . (((len c) + 1) - 1) by A2, A62, A64, FINSEQ_1:24
.= c . (len c) ;
then a in h . (len c) by A20, A63;
then A65: a in (f . (len c)) /\ (f . ((len c) + 1)) by A11, A63;
A66: f . (len f) in rng f by A9, FUNCT_1:def 3;
then reconsider ff = f . (len f) as Subset of S by A22;
A67: ( ff is closed_under_lines & ff is strong ) by A7, A66;
len c = len h by A20, FINSEQ_3:29;
then A68: a in ff by A11, A65, XBOOLE_0:def 4;
b = y by A36, A62, A64, FINSEQ_1:42;
hence a,b are_collinear by A6, A67, A68; :: thesis: verum
end;
end;
end;