theorem :: ANPROJ_8:57
ProjectiveSpace (TOP-REAL 3) is CollProjectivePlane