theorem :: PAPPUS:18

ProjectiveSpace (TOP-REAL 3) is Desarguesian Pappian CollProjectivePlane by ANPROJ_8:57;