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