theorem :: BKMODEL1:71

ProjectiveSpace (TOP-REAL 3) is proper by ANPROJ_8:57;