theorem :: AFPROJ:17

for AS being AffinSpace st AS is AffinPlane holds
AfLines AS misses Dir_of_Planes AS