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:
now :: thesis: for x being Point of S ex l being Block of S st x in l
consider 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 b2
( X1 is closed_under_lines & X1 is strong ) by ;
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 ;
A7: len f in dom f by ;
then reconsider l = (len f) - 1 as Nat by FINSEQ_3:26;
A8: f . (len f) in rng f by ;
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 x in X ; :: thesis: ex l being Block of S st l in b2
hence ex l being Block of S st x in l ; :: thesis: verum
end;
suppose A10: not x in X ; :: thesis: ex l being Block of S st l in b2
1 <= len f by ;
then 1 < ((len f) - 1) + 1 by ;
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 ;
then reconsider a = a as Point of S ;
x,a are_collinear by ;
then consider l being Block of S such that
A14: {x,a} c= l by ;
x in l by ;
hence ex l being Block of S st x in l ; :: thesis: verum
end;
end;
end;
hence S is without_isolated_points by PENCIL_1:def 9; :: thesis: verum