let X be non empty set ; :: thesis: ( 3 c= card X implies for S being TopStruct st the carrier of S = X & the topology of S = { L where L is Subset of X : 2 = card L } holds
( not S is empty & not S is void & not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points ) )
assume A1: 3 c= card X ; :: thesis: for S being TopStruct st the carrier of S = X & the topology of S = { L where L is Subset of X : 2 = card L } holds
( not S is empty & not S is void & not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
A2: Segm 2 c= Segm 3 by NAT_1:39;
then 2 c= card X by A1;
then consider x, y being object such that
A3: ( x in X & y in X ) and
A4: x <> y by Th2;
{x,y} c= X by A3, TARSKI:def 2;
then reconsider l = {x,y} as Subset of X ;
let S be TopStruct ; :: thesis: ( the carrier of S = X & the topology of S = { L where L is Subset of X : 2 = card L } implies ( not S is empty & not S is void & not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points ) )
assume that
A5: the carrier of S = X and
A6: the topology of S = { L where L is Subset of X : 2 = card L } ; :: thesis: ( not S is empty & not S is void & not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
thus not S is empty by A5; :: thesis: ( not S is void & not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
2 = card l by A4, CARD_2:57;
then A7: l in the topology of S by A6;
then reconsider F = { L where L is Subset of X : 2 = card L } as non empty set by A6;
thus not S is void by A7; :: thesis: ( not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
now :: thesis: not X in F
assume X in F ; :: thesis: contradiction
then ex L being Subset of X st
( X = L & 2 = card L ) ;
then Segm 3 c= Segm 2 by A1;
hence contradiction by NAT_1:39; :: thesis: verum
end;
then X is not Element of F ;
hence not S is degenerated by A5, A6; :: thesis: ( not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
for x, y being Point of S holds x,y are_collinear
proof
let x, y be Point of S; :: thesis: x,y are_collinear
per cases ( x = y or x <> y ) ;
suppose A8: x = y ; :: thesis: x,y are_collinear
consider z being object such that
A9: z in X and
A10: z <> x by A1, A2, Th3, XBOOLE_1:1;
reconsider z = z as Point of S by A5, A9;
A11: {x,y} c= {x,z}
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {x,y} or a in {x,z} )
assume a in {x,y} ; :: thesis: a in {x,z}
then ( a = x or a = y ) by TARSKI:def 2;
hence a in {x,z} by A8, TARSKI:def 2; :: thesis: verum
end;
{x,z} c= X
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {x,z} or a in X )
assume a in {x,z} ; :: thesis: a in X
then ( a = x or a = z ) by TARSKI:def 2;
hence a in X by A5; :: thesis: verum
end;
then reconsider l = {x,z} as Subset of X ;
card l = 2 by A10, CARD_2:57;
then l in the topology of S by A6;
hence x,y are_collinear by A11; :: thesis: verum
end;
suppose A12: x <> y ; :: thesis: x,y are_collinear
{x,y} c= X
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {x,y} or a in X )
assume a in {x,y} ; :: thesis: a in X
then ( a = x or a = y ) by TARSKI:def 2;
hence a in X by A5; :: thesis: verum
end;
then reconsider l = {x,y} as Subset of X ;
card {x,y} = 2 by A12, CARD_2:57;
then l in the topology of S by A6;
hence x,y are_collinear ; :: thesis: verum
end;
end;
end;
hence not S is truly-partial ; :: thesis: ( S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
thus S is with_non_trivial_blocks :: thesis: ( S is identifying_close_blocks & S is without_isolated_points )
proof
let k be Block of S; :: according to PENCIL_1:def 6 :: thesis: 2 c= card k
k in the topology of S by A7;
then ex m being Subset of X st
( m = k & card m = 2 ) by A6;
hence 2 c= card k ; :: thesis: verum
end;
thus S is identifying_close_blocks :: thesis: S is without_isolated_points
proof
let k, l be Block of S; :: according to PENCIL_1:def 7 :: thesis: ( 2 c= card (k /\ l) implies k = l )
assume 2 c= card (k /\ l) ; :: thesis: k = l
then consider a, b being object such that
A13: ( a in k /\ l & b in k /\ l ) and
A14: a <> b by Th2;
A15: {a,b} c= k /\ l by A13, TARSKI:def 2;
l in the topology of S by A7;
then A16: ex n being Subset of X st
( n = l & card n = 2 ) by A6;
then reconsider l1 = l as finite set ;
A17: k /\ l c= l1 by XBOOLE_1:17;
k in the topology of S by A7;
then A18: ex m being Subset of X st
( m = k & card m = 2 ) by A6;
then reconsider k1 = k as finite set ;
A19: card {a,b} = 2 by A14, CARD_2:57;
k /\ l c= k1 by XBOOLE_1:17;
then {a,b} = k1 by A18, A15, A19, CARD_2:102, XBOOLE_1:1;
hence k = l by A15, A19, A16, A17, CARD_2:102, XBOOLE_1:1; :: thesis: verum
end;
thus S is without_isolated_points :: thesis: verum
proof
let x be Point of S; :: according to PENCIL_1:def 9 :: thesis: ex l being Block of S st x in l
consider z being object such that
A20: z in X and
A21: z <> x by A1, A2, Th3, XBOOLE_1:1;
{x,z} c= X
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {x,z} or a in X )
assume a in {x,z} ; :: thesis: a in X
then ( a = x or a = z ) by TARSKI:def 2;
hence a in X by A5, A20; :: thesis: verum
end;
then reconsider l = {x,z} as Subset of X ;
card {x,z} = 2 by A21, CARD_2:57;
then l in the topology of S by A6;
then reconsider l = l as Block of S ;
take l ; :: thesis: x in l
thus x in l by TARSKI:def 2; :: thesis: verum
end;