let S be non void identifying_close_blocks TopStruct ; :: thesis: ( S is strongly_connected implies S is without_isolated_points )

assume A1: S is strongly_connected ; :: thesis: S is without_isolated_points

assume A1: S is strongly_connected ; :: thesis: S is without_isolated_points

now :: thesis: for x being Point of S ex l being Block of S st x in l

hence
S is without_isolated_points
by PENCIL_1:def 9; :: thesis: verumconsider X being object such that

A2: X in the topology of S by XBOOLE_0:def 1;

reconsider X = X as Block of S by A2;

reconsider X1 = X as Subset of S by A2;

let x be Point of S; :: thesis: ex l being Block of S st l in b_{2}

( X1 is closed_under_lines & X1 is strong ) by PENCIL_1:20, PENCIL_1:21;

then consider f being FinSequence of bool the carrier of S such that

A3: X = f . 1 and

A4: x in f . (len f) and

A5: for W being Subset of S st W in rng f holds

( W is closed_under_lines & W is strong ) and

A6: for i being Nat st 1 <= i & i < len f holds

2 c= card ((f . i) /\ (f . (i + 1))) by A1, PENCIL_1:def 11;

A7: len f in dom f by A4, FUNCT_1:def 2;

then reconsider l = (len f) - 1 as Nat by FINSEQ_3:26;

A8: f . (len f) in rng f by A7, FUNCT_1:3;

then reconsider W = f . (len f) as Subset of S ;

A9: ( W is closed_under_lines & W is strong ) by A5, A8;

end;A2: X in the topology of S by XBOOLE_0:def 1;

reconsider X = X as Block of S by A2;

reconsider X1 = X as Subset of S by A2;

let x be Point of S; :: thesis: ex l being Block of S st l in b

( X1 is closed_under_lines & X1 is strong ) by PENCIL_1:20, PENCIL_1:21;

then consider f being FinSequence of bool the carrier of S such that

A3: X = f . 1 and

A4: x in f . (len f) and

A5: for W being Subset of S st W in rng f holds

( W is closed_under_lines & W is strong ) and

A6: for i being Nat st 1 <= i & i < len f holds

2 c= card ((f . i) /\ (f . (i + 1))) by A1, PENCIL_1:def 11;

A7: len f in dom f by A4, FUNCT_1:def 2;

then reconsider l = (len f) - 1 as Nat by FINSEQ_3:26;

A8: f . (len f) in rng f by A7, FUNCT_1:3;

then reconsider W = f . (len f) as Subset of S ;

A9: ( W is closed_under_lines & W is strong ) by A5, A8;

per cases
( x in X or not x in X )
;

end;

suppose A10:
not x in X
; :: thesis: ex l being Block of S st l in b_{2}

1 <= len f
by A7, FINSEQ_3:25;

then 1 < ((len f) - 1) + 1 by A3, A4, A10, XXREAL_0:1;

then ( 1 <= l & l < len f ) by NAT_1:13;

then 2 c= card ((f . l) /\ (f . (l + 1))) by A6;

then consider a being object such that

A11: a in (f . l) /\ (f . (len f)) and

A12: a <> x by PENCIL_1:3;

A13: a in W by A11, XBOOLE_0:def 4;

then reconsider a = a as Point of S ;

x,a are_collinear by A4, A9, A13, PENCIL_1:def 3;

then consider l being Block of S such that

A14: {x,a} c= l by A12, PENCIL_1:def 1;

x in l by A14, ZFMISC_1:32;

hence ex l being Block of S st x in l ; :: thesis: verum

end;then 1 < ((len f) - 1) + 1 by A3, A4, A10, XXREAL_0:1;

then ( 1 <= l & l < len f ) by NAT_1:13;

then 2 c= card ((f . l) /\ (f . (l + 1))) by A6;

then consider a being object such that

A11: a in (f . l) /\ (f . (len f)) and

A12: a <> x by PENCIL_1:3;

A13: a in W by A11, XBOOLE_0:def 4;

then reconsider a = a as Point of S ;

x,a are_collinear by A4, A9, A13, PENCIL_1:def 3;

then consider l being Block of S such that

A14: {x,a} c= l by A12, PENCIL_1:def 1;

x in l by A14, ZFMISC_1:32;

hence ex l being Block of S st x in l ; :: thesis: verum