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
now let x be
Point of
S;
:: thesis: ex l being Block of S st l in b2consider X being
set 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;
(
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 &
x in f . (len f) & ( for
W being
Subset of
S st
W in rng f holds
(
W is
closed_under_lines &
W is
strong ) ) & ( 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;
A4:
len f in dom f
by A3, FUNCT_1:def 4;
then A5:
f . (len f) in rng f
by FUNCT_1:12;
then reconsider W =
f . (len f) as
Subset of
S ;
A6:
(
W is
closed_under_lines &
W is
strong & ( for
i being
Nat st 1
<= i &
i < len f holds
2
c= card ((f . i) /\ (f . (i + 1))) ) )
by A3, A5;
reconsider l =
(len f) - 1 as
Nat by A4, FINSEQ_3:28;
per cases
( x in X or not x in X )
;
suppose A7:
not
x in X
;
:: thesis: ex l being Block of S st l in b2
1
<= len f
by A4, FINSEQ_3:27;
then
1
< ((len f) - 1) + 1
by A3, A7, XXREAL_0:1;
then
( 1
<= l &
l < len f )
by NAT_1:13;
then
2
c= card ((f . l) /\ (f . (l + 1)))
by A3;
then consider a being
set such that A8:
(
a in (f . l) /\ (f . (len f)) &
a <> x )
by PENCIL_1:3;
A9:
(
a in W &
a <> x )
by A8, XBOOLE_0:def 4;
then reconsider a =
a as
Point of
S ;
x,
a are_collinear
by A3, A6, A9, PENCIL_1:def 3;
then consider l being
Block of
S such that A10:
{x,a} c= l
by A8, PENCIL_1:def 1;
(
x in l &
a in l )
by A10, ZFMISC_1:38;
hence
ex
l being
Block of
S st
x in l
;
:: thesis: verum end;
hence
S is without_isolated_points
by PENCIL_1:def 9; :: thesis: verum