let X be non empty set ; :: thesis: ( 3 c= card X implies for K being Subset of X st card K = 2 holds
for S being TopStruct st the carrier of S = X & the topology of S = { L where L is Subset of X : 2 = card L } \ {K} holds
( not S is empty & not S is void & not S is degenerated & 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 K being Subset of X st card K = 2 holds
for S being TopStruct st the carrier of S = X & the topology of S = { L where L is Subset of X : 2 = card L } \ {K} holds
( not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
let K be Subset of X; :: thesis: ( card K = 2 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 } \ {K} holds
( not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points ) )
assume A2: card K = 2 ; :: 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 } \ {K} holds
( not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
then reconsider K9 = K as finite Subset of X ;
consider x, y being object such that
A3: x <> y and
A4: K9 = {x,y} by A2, CARD_2:60;
let S be TopStruct ; :: thesis: ( the carrier of S = X & the topology of S = { L where L is Subset of X : 2 = card L } \ {K} implies ( not S is empty & not S is void & not S is degenerated & 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 } \ {K} ; :: thesis: ( not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
reconsider x = x, y = y as Point of S by A5, A4, ZFMISC_1:32;
consider z being object such that
A7: z in X and
A8: z <> x and
A9: z <> y by A1, Th6;
{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, A7; :: thesis: verum
end;
then reconsider l = {x,z} as Subset of X ;
card l = 2 by A8, CARD_2:57;
then A10: ( z in l & l in { L where L is Subset of X : 2 = card L } ) by TARSKI:def 2;
thus not S is empty by A5; :: thesis: ( not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
not z in K9 by A4, A8, A9, TARSKI:def 2;
then A11: not { L where L is Subset of X : 2 = card L } c= {K} by A10, TARSKI:def 1;
then A12: not { L where L is Subset of X : 2 = card L } \ {K} is empty by XBOOLE_1:37;
hence not S is void by A6; :: thesis: ( not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
reconsider F = { L where L is Subset of X : 2 = card L } \ {K} as non empty set by A11, XBOOLE_1:37;
now :: thesis: not X in F
assume X in F ; :: thesis: contradiction
then X in { L where L is Subset of X : 2 = card L } ;
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: ( S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
thus S is truly-partial :: thesis: ( S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
proof
take x ; :: according to PENCIL_1:def 8 :: thesis: not for y being Point of S holds x,y are_collinear
take y ; :: thesis: not x,y are_collinear
for l being Block of S holds not {x,y} c= l
proof
let l be Block of S; :: thesis: not {x,y} c= l
l in { L where L is Subset of X : 2 = card L } by A6, A12, XBOOLE_0:def 5;
then consider L being Subset of X such that
A13: l = L and
A14: card L = 2 ;
reconsider L9 = L as finite Subset of X by A14;
consider a, b being object such that
a <> b and
A15: L9 = {a,b} by A14, CARD_2:60;
A16: not l in {K} by A6, A12, XBOOLE_0:def 5;
hence not {x,y} c= l ; :: thesis: verum
end;
hence not x,y are_collinear by A3; :: thesis: verum
end;
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 { L where L is Subset of X : 2 = card L } by A6, A12, XBOOLE_0:def 5;
then ex m being Subset of X st
( m = k & card m = 2 ) ;
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
A19: ( a in k /\ l & b in k /\ l ) and
A20: a <> b by Th2;
A21: {a,b} c= k /\ l by A19, TARSKI:def 2;
l in { L where L is Subset of X : 2 = card L } by A6, A12, XBOOLE_0:def 5;
then A22: ex n being Subset of X st
( n = l & card n = 2 ) ;
then reconsider l1 = l as finite set ;
A23: k /\ l c= l1 by XBOOLE_1:17;
k in { L where L is Subset of X : 2 = card L } by A6, A12, XBOOLE_0:def 5;
then A24: ex m being Subset of X st
( m = k & card m = 2 ) ;
then reconsider k1 = k as finite set ;
A25: card {a,b} = 2 by A20, CARD_2:57;
k /\ l c= k1 by XBOOLE_1:17;
then {a,b} = k1 by A24, A21, A25, CARD_2:102, XBOOLE_1:1;
hence k = l by A21, A25, A22, A23, CARD_2:102, XBOOLE_1:1; :: thesis: verum
end;
A26: Segm 2 c= Segm 3 by NAT_1:39;
thus S is without_isolated_points :: thesis: verum
proof
let p be Point of S; :: according to PENCIL_1:def 9 :: thesis: ex l being Block of S st p in l
per cases ( ( p <> x & p <> y ) or p = x or p = y ) ;
suppose A27: ( p <> x & p <> y ) ; :: thesis: ex l being Block of S st p in l
consider z being object such that
A28: z in X and
A29: z <> p by A1, A26, Th3, XBOOLE_1:1;
{p,z} c= X
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {p,z} or a in X )
assume a in {p,z} ; :: thesis: a in X
then ( a = p or a = z ) by TARSKI:def 2;
hence a in X by A5, A28; :: thesis: verum
end;
then reconsider el = {p,z} as Subset of X ;
card {p,z} = 2 by A29, CARD_2:57;
then A30: el in { L where L is Subset of X : 2 = card L } ;
p in el by TARSKI:def 2;
then el <> K by A4, A27, TARSKI:def 2;
then not el in {K} by TARSKI:def 1;
then reconsider el = el as Block of S by A6, A30, XBOOLE_0:def 5;
take el ; :: thesis: p in el
thus p in el by TARSKI:def 2; :: thesis: verum
end;
suppose A31: ( p = x or p = y ) ; :: thesis: ex l being Block of S st p in l
consider z being object such that
A32: z in X and
A33: ( z <> x & z <> y ) by A1, Th6;
{p,z} c= X
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {p,z} or a in X )
assume a in {p,z} ; :: thesis: a in X
then ( a = p or a = z ) by TARSKI:def 2;
hence a in X by A5, A32; :: thesis: verum
end;
then reconsider el = {p,z} as Subset of X ;
card {p,z} = 2 by A31, A33, CARD_2:57;
then A34: el in { L where L is Subset of X : 2 = card L } ;
z in el by TARSKI:def 2;
then el <> K by A4, A33, TARSKI:def 2;
then not el in {K} by TARSKI:def 1;
then reconsider el = el as Block of S by A6, A34, XBOOLE_0:def 5;
take el ; :: thesis: p in el
thus p in el by TARSKI:def 2; :: thesis: verum
end;
end;
end;