theorem :: ANPROJ_1:23

for V being non trivial RealLinearSpace holds
( the carrier of (ProjectiveSpace V) = ProjectivePoints V & the Collinearity of (ProjectiveSpace V) = ProjectiveCollinearity V ) ;