theorem :: ANPROJ_8:57

ProjectiveSpace (TOP-REAL 3) is CollProjectivePlane