:: deftheorem defines ProjectiveLines AFPROJ:def 10 :
for AS being AffinSpace holds ProjectiveLines AS = [:(AfLines AS),{1}:] \/ [:(Dir_of_Planes AS),{2}:];