let X be non empty set ; :: thesis:
assume A1: 3 c= card X ; :: thesis:
B2: 2 c= 3 by NAT_1:40;
let K be Subset of X; :: thesis:
assume A3: card K = 2 ; :: thesis:
then card K = card 2 ;
then reconsider K' = K as finite Subset of X ;
let S be TopStruct ; :: thesis:
assume that
A4: the carrier of S = X and
A5: the topology of S = { L where L is Subset of X : 2 = card L } \ {K} ; :: thesis:
consider x, y being set such that
A6: ( x <> y & K' = {x,y} ) by A3, CARD_2:79;
reconsider x = x, y = y as Point of S by A4, A6, ZFMISC_1:38;
thus not S is empty by A4; :: thesis:
consider z being set such that
A7: ( z in X & z <> x & z <> y ) by A1, Th6;
{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 A4, A7; :: thesis:

end;

then reconsider l = {x,z} as Subset of X ;
A8: ( not z in K' & z in l ) by A6, A7, TARSKI:def 2;
card l = 2 by A7, CARD_2:76;
then ( l in { L where L is Subset of X : 2 = card L } & not l in {K} ) by A8, TARSKI:def 1;
then A9: not { L where L is Subset of X : 2 = card L } c= {K} ;
then A10: not { L where L is Subset of X : 2 = card L } \ {K} is empty by XBOOLE_1:37;
hence not S is void by A5, Def4; :: thesis:
reconsider F = { L where L is Subset of X : 2 = card L } \ {K} as non empty set by A9, XBOOLE_1:37;

now

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

end;

then X is not Element of F ;
hence not S is degenerated by A4, A5, Def5; :: thesis:
thus S is truly-partial :: thesis:

proof

take x ; :: according to PENCIL_1:def 8 :: thesis:
take y ; :: thesis:
for l being Block of S holds not {x,y} c= l

proof

let l be Block of S; :: thesis:
A12: ( l in { L where L is Subset of X : 2 = card L } & not l in {K} ) by A5, A10, XBOOLE_0:def 5;
then consider L being Subset of X such that
A13: ( l = L & card L = 2 ) ;
card L = card 2 by A13;
then reconsider L' = L as finite Subset of X ;
consider a, b being set such that
A14: ( a <> b & L' = {a,b} ) by A13, CARD_2:79;

now

assume {x,y} c= l ; :: thesis:
then ( x in L' & y in L' ) by A13, ZFMISC_1:38;
then ( ( x = a or x = b ) & ( y = a or y = b ) ) by A14, TARSKI:def 2;
hence contradiction by A6, A12, A13, A14, TARSKI:def 1; :: thesis:

end;

hence not {x,y} c= l ; :: thesis:

end;

hence not x,y are_collinear by A6, Def1; :: thesis:

end;

thus S is with_non_trivial_blocks :: thesis:

proof

let k be Block of S; :: according to PENCIL_1:def 6 :: thesis:
k in { L where L is Subset of X : 2 = card L } by A5, A10, XBOOLE_0:def 5;
then consider m being Subset of X such that
A15: ( m = k & card m = 2 ) ;
thus 2 c= card k by A15; :: 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 { L where L is Subset of X : 2 = card L } by A5, A10, XBOOLE_0:def 5;
then consider m being Subset of X such that
A16: ( m = k & card m = 2 ) ;
assume 2 c= card (k /\ l) ; :: thesis:
then consider a, b being set such that
A17: ( a in k /\ l & b in k /\ l & a <> b ) by Th2;
A18: {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 A17, TARSKI:def 2; :: thesis:

end;

A19: card {a,b} = 2 by A17, CARD_2:76;
card k = card 2 by A16;
then reconsider k1 = k as finite set ;
k /\ l c= k1 by XBOOLE_1:17;
then A20: {a,b} = k1 by A16, A18, A19, TRIANG_1:3, XBOOLE_1:1;
l in { L where L is Subset of X : 2 = card L } by A5, A10, XBOOLE_0:def 5;
then consider n being Subset of X such that
A21: ( n = l & card n = 2 ) ;
card l = card 2 by A21;
then reconsider l1 = l as finite set ;
k /\ l c= l1 by XBOOLE_1:17;
hence k = l by A18, A19, A20, A21, TRIANG_1:3, XBOOLE_1:1; :: thesis:

end;

thus S is without_isolated_points :: thesis:

proof

let p be Point of S; :: according to PENCIL_1:def 9 :: thesis:

per cases ;

suppose A22: ( p <> x & p <> y ) ; :: thesis:

consider z being set such that
A23: ( z in X & z <> p ) by B2, Th3, A1, XBOOLE_1:1;
A24: card {p,z} = 2 by A23, CARD_2:76;
{p,z} c= X

proof

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

end;

then reconsider el = {p,z} as Subset of X ;
p in el by TARSKI:def 2;
then el <> K by A6, A22, TARSKI:def 2;
then ( el in { L where L is Subset of X : 2 = card L } & not el in {K} ) by A24, TARSKI:def 1;
then reconsider el = el as Block of S by A5, XBOOLE_0:def 5;
take el ; :: thesis:
thus p in el by TARSKI:def 2; :: thesis:

end;

suppose A25: ( p = x or p = y ) ; :: thesis:

consider z being set such that
A26: ( z in X & z <> x & z <> y ) by A1, Th6;
A27: card {p,z} = 2 by A25, A26, CARD_2:76;
{p,z} c= X

proof

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

end;

then reconsider el = {p,z} as Subset of X ;
z in el by TARSKI:def 2;
then el <> K by A6, A26, TARSKI:def 2;
then ( el in { L where L is Subset of X : 2 = card L } & not el in {K} ) by A27, TARSKI:def 1;
then reconsider el = el as Block of S by A5, XBOOLE_0:def 5;
take el ; :: thesis:
thus p in el by TARSKI:def 2; :: thesis:

end;