:: deftheorem defines ProjectiveSpace ANPROJ_1:def 7 :
for V being non trivial RealLinearSpace holds ProjectiveSpace V = CollStr(# (ProjectivePoints V),(ProjectiveCollinearity V) #);