let K, L be Block of (VeroneseSpace S); PENCIL_1:def 7 ( not 2 c= card (K /\ L) or K = L )
assume
2 c= card (K /\ L)
; K = L
then consider a, b being object such that
A1:
a in K /\ L
and
A2:
b in K /\ L
and
A3:
a <> b
by PENCIL_1:2;
A4:
a in K
by A1, XBOOLE_0:def 4;
then A5:
not the topology of (VeroneseSpace S) is empty
by SUBSET_1:def 1;
then consider t being set , k being Subset of S such that
t in the carrier of S
and
A6:
k in the topology of S
and
A7:
K = PairSet (t,k)
by Def10;
b in K
by A2, XBOOLE_0:def 4;
then consider y being set such that
A8:
y in k
and
A9:
b = {t,y}
by A7, Def9;
consider x being set such that
A10:
x in k
and
A11:
a = {t,x}
by A4, A7, Def9;
consider s being set , l being Subset of S such that
s in the carrier of S
and
A12:
l in the topology of S
and
A13:
L = PairSet (s,l)
by A5, Def10;
a in L
by A1, XBOOLE_0:def 4;
then consider z being set such that
A14:
z in l
and
A15:
a = {s,z}
by A13, Def9;
b in L
by A2, XBOOLE_0:def 4;
then consider w being set such that
A16:
w in l
and
A17:
b = {s,w}
by A13, Def9;
A18:
( t = s or t = z )
by A11, A15, ZFMISC_1:6;
then A20:
y in k /\ l
by A8, A16, XBOOLE_0:def 4;
A21:
( t = s or t = w )
by A9, A17, ZFMISC_1:6;
then
x in k /\ l
by A10, A14, XBOOLE_0:def 4;
then
2 c= card (k /\ l)
by A3, A11, A9, A20, PENCIL_1:2;
hence
K = L
by A3, A6, A7, A12, A13, A15, A17, A18, A21, PENCIL_1:def 7; verum