:: deftheorem defines real_projective_plane BKMODEL1:def 4 :
real_projective_plane = ProjectiveSpace (TOP-REAL 3);