:: deftheorem defines PDir AFPROJ:def 6 :
for AS being AffinSpace
for X being Subset of AS holds PDir X = Class ((PlanesParallelity AS),X);