let X be non empty set ; :: thesis:
assume A1: 3 c= card X ; :: thesis:
B2: 2 c= 3 by NAT_1:40;
then A2: 2 c= card X by A1, XBOOLE_1:1;
let S be TopStruct ; :: thesis:
assume that
A3: the carrier of S = X and
A4: the topology of S = { L where L is Subset of X : 2 = card L } ; :: thesis:
thus not S is empty by A3; :: thesis:
consider x, y being set such that
A5: ( x in X & y in X & x <> y ) by A2, Th2;
{x,y} c= X

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in {x,y} ; :: thesis:
hence a in X by A5, TARSKI:def 2; :: thesis:

end;

then reconsider l = {x,y} as Subset of X ;
2 = card l by A5, CARD_2:76;
then A6: l in the topology of S by A4;
hence not S is void by Def4; :: thesis:
reconsider F = { L where L is Subset of X : 2 = card L } as non empty set by A4, A6;

now

assume X in F ; :: thesis:
then consider L being Subset of X such that
A7: ( X = L & 2 = card L ) ;
thus contradiction by A1, A7, NAT_1:40; :: thesis:

end;

then X is not Element of F ;
hence not S is degenerated by A3, A4, Def5; :: thesis:
for x, y being Point of S holds x,y are_collinear

proof

let x, y be Point of S; :: thesis:

per cases ;

suppose A8: x = y ; :: thesis:

consider z being set such that
A9: ( z in X & z <> x ) by B2, Th3, A1, XBOOLE_1:1;
reconsider z = z as Point of S by A3, A9;
A10: {x,y} c= {x,z}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in {x,y} ; :: thesis:
then ( a = x or a = y ) by TARSKI:def 2;
hence a in {x,z} by A8, TARSKI:def 2; :: thesis:

end;

{x,z} c= X

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in {x,z} ; :: thesis:
then ( a = x or a = z ) by TARSKI:def 2;
hence a in X by A3; :: thesis:

end;

then reconsider l = {x,z} as Subset of X ;
card l = 2 by A9, CARD_2:76;
then l in the topology of S by A4;
hence x,y are_collinear by A10, Def1; :: thesis:

end;

suppose x <> y ; :: thesis:

then A11: card {x,y} = 2 by CARD_2:76;
{x,y} c= X

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in {x,y} ; :: thesis:
then ( a = x or a = y ) by TARSKI:def 2;
hence a in X by A3; :: thesis:

end;

then reconsider l = {x,y} as Subset of X ;
l in the topology of S by A4, A11;
hence x,y are_collinear by Def1; :: thesis:

end;

hence not S is truly-partial by Def8; :: thesis:
thus S is with_non_trivial_blocks :: thesis:

proof

let k be Block of S; :: according to PENCIL_1:def 6 :: thesis:
k in the topology of S by A6;
then consider m being Subset of X such that
A12: ( m = k & card m = 2 ) by A4;
thus 2 c= card k by A12; :: thesis:

end;

thus S is identifying_close_blocks :: thesis:

proof

let k, l be Block of S; :: according to PENCIL_1:def 7 :: thesis:
k in the topology of S by A6;
then consider m being Subset of X such that
A13: ( m = k & card m = 2 ) by A4;
assume 2 c= card (k /\ l) ; :: thesis:
then consider a, b being set such that
A14: ( a in k /\ l & b in k /\ l & a <> b ) by Th2;
A15: {a,b} c= k /\ l

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in {a,b} ; :: thesis:
hence x in k /\ l by A14, TARSKI:def 2; :: thesis:

end;

A16: card {a,b} = 2 by A14, CARD_2:76;
card k = card 2 by A13;
then reconsider k1 = k as finite set ;
k /\ l c= k1 by XBOOLE_1:17;
then A17: {a,b} = k1 by A13, A15, A16, TRIANG_1:3, XBOOLE_1:1;
l in the topology of S by A6;
then consider n being Subset of X such that
A18: ( n = l & card n = 2 ) by A4;
card l = card 2 by A18;
then reconsider l1 = l as finite set ;
k /\ l c= l1 by XBOOLE_1:17;
hence k = l by A15, A16, A17, A18, TRIANG_1:3, XBOOLE_1:1; :: thesis:

end;

thus S is without_isolated_points :: thesis:

proof

let x be Point of S; :: according to PENCIL_1:def 9 :: thesis:
consider z being set such that
A19: ( z in X & z <> x ) by B2, Th3, A1, XBOOLE_1:1;
A20: card {x,z} = 2 by A19, CARD_2:76;
{x,z} c= X

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in {x,z} ; :: thesis:
then ( a = x or a = z ) by TARSKI:def 2;
hence a in X by A3, A19; :: thesis:

end;

then reconsider l = {x,z} as Subset of X ;
l in the topology of S by A4, A20;
then reconsider l = l as Block of S ;
take l ; :: thesis:
thus x in l by TARSKI:def 2; :: thesis:

end;