theorem :: AFPROJ:33

for AS being AffinSpace
for X being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st A = [(PDir X),2] & X is being_plane & a on A holds
not a is Element of AS by Th27;