let K, L be Block of (VeroneseSpace S); :: according to PENCIL_1:def 7 :: thesis: ( not 2 c= card (K /\ L) or K = L )
assume 2 c= card (K /\ L) ; :: thesis: K = L
then consider a, b being set such that
A1: ( a in K /\ L & b in K /\ L & a <> b ) by PENCIL_1:2;
A2: ( a in K & a in L & b in K & b in L ) by A1, XBOOLE_0:def 4;
then A3: not the topology of (VeroneseSpace S) is empty by SUBSET_1:def 2;
then consider t being set , k being Subset of S such that
A4: ( t in the carrier of S & k in the topology of S & K = PairSet t,k ) by Def10;
consider s being set , l being Subset of S such that
A5: ( s in the carrier of S & l in the topology of S & L = PairSet s,l ) by A3, Def10;
consider x being set such that
A6: ( x in k & a = {t,x} ) by A2, A4, Def9;
consider y being set such that
A7: ( y in k & b = {t,y} ) by A2, A4, Def9;
consider z being set such that
A8: ( z in l & a = {s,z} ) by A2, A5, Def9;
consider w being set such that
A9: ( w in l & b = {s,w} ) by A2, A5, Def9;
A10: ( ( t = s or t = z ) & ( t = s or t = w ) ) by A6, A7, A8, A9, ZFMISC_1:10;

A11: now

assume A12: x <> z ; :: thesis: contradiction
then x = t by A1, A6, A8, A9, A10, ZFMISC_1:10;
hence contradiction by A6, A8, A12, ZFMISC_1:10; :: thesis: verum

end;

now

assume A13: y <> w ; :: thesis: contradiction
then y = t by A1, A7, A8, A9, A10, ZFMISC_1:10;
hence contradiction by A7, A9, A13, ZFMISC_1:10; :: thesis: verum

end;

then ( x in k /\ l & y in k /\ l ) by A6, A7, A8, A9, A11, XBOOLE_0:def 4;
then 2 c= card (k /\ l) by A1, A6, A7, PENCIL_1:2;
hence K = L by A1, A4, A5, A8, A9, A10, PENCIL_1:def 7; :: thesis: verum