let S be non void identifying_close_blocks TopStruct ; ( S is strongly_connected implies S is without_isolated_points )
assume A1:
S is strongly_connected
; S is without_isolated_points
now for x being Point of S ex l being Block of S st x in lconsider 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;
ex l being Block of S st l in b2
(
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 )
;
suppose A10:
not
x in X
;
ex l being Block of S st l in b2
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
;
verum end;
hence
S is without_isolated_points
by PENCIL_1:def 9; verum