theorem Th34: :: AFPROJ:34

for AS being AffinSpace
for X being Subset of AS
for p being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st A = [X,1] & X is being_line & p on A & p is not Element of AS holds
p = LDir X