theorem Th62: :: BKMODEL1:75

IncProjSp_of real_projective_plane is IncProjectivePlane