:: deftheorem defines ProjectivePoints AFPROJ:def 9 :
for AS being AffinSpace holds ProjectivePoints AS = the carrier of AS \/ (Dir_of_Lines AS);