theorem Th31: :: AFPROJ:31

for AS being AffinSpace
for X, Y being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st X is being_line & Y is being_plane & X c= Y & a = LDir X & A = [(PDir Y),2] holds
a on A