:: deftheorem defines VeroneseSpace PENCIL_4:def 11 :
for S being TopStruct holds VeroneseSpace S = TopStruct(# (PairSet the carrier of S),(PairSetFamily the topology of S) #);