:: deftheorem defines ProjHorizon AFPROJ:def 14 :
for AS being AffinSpace holds ProjHorizon AS = IncProjStr(# (Dir_of_Lines AS),(Dir_of_Planes AS),(Inc_of_Dir AS) #);