assume the carrier of (VeroneseSpace S) is Block of (VeroneseSpace S) ; :: according to PENCIL_1:def 5 :: thesis: contradiction
then consider t being set , l being Subset of S such that
A1: t in the carrier of S and
A2: l in the topology of S and
A3: PairSet the carrier of S = PairSet (t,l) by Def10;
not the carrier of S in the topology of S by PENCIL_1:def 5;
then not the carrier of S c= l by A2, XBOOLE_0:def 10;
then consider s being object such that
A4: s in the carrier of S and
A5: not s in l ;
now :: thesis: not {t,s} in PairSet (t,l)
assume {t,s} in PairSet (t,l) ; :: thesis: contradiction
then A6: ex z being set st
( z in l & {t,s} = {t,z} ) by Def9;
then s = t by A5, ZFMISC_1:6;
hence contradiction by A5, A6, ZFMISC_1:6; :: thesis: verum
end;
hence contradiction by A1, A3, A4, Def8; :: thesis: verum