theorem Th43: :: AFPROJ:43

for AS being AffinSpace
for X, Y, X9 being Subset of AS
for P, Q being LINE of (IncProjSp_of AS) st Y is being_plane & X is being_line & X9 is being_line & X c= Y & X9 c= Y & P = [X,1] & Q = [X9,1] holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )