:: deftheorem defines IncProjSp_of AFPROJ:def 13 :
for AS being AffinSpace holds IncProjSp_of AS = IncProjStr(# (ProjectivePoints AS),(ProjectiveLines AS),(Proj_Inc AS) #);