let AS be AffinSpace; :: thesis: 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
let X, Y, X9 be Subset of AS; :: thesis: 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
let a be POINT of (IncProjSp_of AS); :: thesis: 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
let A be LINE of (IncProjSp_of AS); :: thesis: ( Y is being_plane & X c= Y & X9 // X & a = LDir X9 & A = [(PDir Y),2] implies a on A )
assume that
A1: Y is being_plane and
A2: X c= Y and
A3: X9 // X and
A4: a = LDir X9 and
A5: A = [(PDir Y),2] ; :: thesis: a on A
X is being_line by A3, AFF_1:36;
then A6: X9 '||' Y by A1, A2, A3, AFF_4:42, AFF_4:56;
X9 is being_line by A3, AFF_1:36;
hence a on A by A1, A4, A5, A6, Th29; :: thesis: verum