IncProjSp_of real_projective_plane is IncProjectivePlane