let X be non empty set ; ( 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
; 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; ( 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
; 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 ; ( 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}
; ( 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
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; ( 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; ( 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;
then
X is not Element of F
;
hence
not S is degenerated
by A5, A6; ( 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
( S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )proof
take
x
;
PENCIL_1:def 8 not for y being Point of S holds x,y are_collinear
take
y
;
not x,y are_collinear
for
l being
Block of
S holds not
{x,y} c= l
proof
let l be
Block of
S;
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;
now not {x,y} c= lassume A17:
{x,y} c= l
;
contradictionthen
y in L9
by A13, ZFMISC_1:32;
then A18:
(
y = a or
y = b )
by A15, TARSKI:def 2;
x in L9
by A13, A17, ZFMISC_1:32;
then
(
x = a or
x = b )
by A15, TARSKI:def 2;
hence
contradiction
by A3, A4, A16, A13, A15, A18, TARSKI:def 1;
verum end;
hence
not
{x,y} c= l
;
verum
end;
hence
not
x,
y are_collinear
by A3;
verum
end;
thus
S is with_non_trivial_blocks
( S is identifying_close_blocks & S is without_isolated_points )
thus
S is identifying_close_blocks
S is without_isolated_points proof
let k,
l be
Block of
S;
PENCIL_1:def 7 ( 2 c= card (k /\ l) implies k = l )
assume
2
c= card (k /\ l)
;
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;
verum
end;
A26:
Segm 2 c= Segm 3
by NAT_1:39;
thus
S is without_isolated_points
verumproof
let p be
Point of
S;
PENCIL_1:def 9 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 )
;
ex l being Block of S st p in lconsider z being
object such that A28:
z in X
and A29:
z <> p
by A1, A26, Th3, XBOOLE_1:1;
{p,z} c= X
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
;
p in elthus
p in el
by TARSKI:def 2;
verum end; suppose A31:
(
p = x or
p = y )
;
ex l being Block of S st p in lconsider z being
object such that A32:
z in X
and A33:
(
z <> x &
z <> y )
by A1, Th6;
{p,z} c= X
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
;
p in elthus
p in el
by TARSKI:def 2;
verum end; end;
end;