let AS be AffinSpace; :: thesis: for Y, X, X' being Subset of
for a being POINT of
for A being LINE of st Y is being_plane & X c= Y & X' // X & a = LDir X' & A = [(PDir Y),2] holds
a on A
let Y, X, X' be Subset of ; :: thesis: for a being POINT of
for A being LINE of st Y is being_plane & X c= Y & X' // X & a = LDir X' & A = [(PDir Y),2] holds
a on A
let a be POINT of ; :: thesis: for A being LINE of st Y is being_plane & X c= Y & X' // X & a = LDir X' & A = [(PDir Y),2] holds
a on A
let A be LINE of ; :: thesis: ( Y is being_plane & X c= Y & X' // X & a = LDir X' & A = [(PDir Y),2] implies a on A )
assume that
A1: Y is being_plane and
A2: X c= Y and
A3: X' // X and
A4: a = LDir X' and
A5: A = [(PDir Y),2] ; :: thesis: a on A
X is being_line by A3, AFF_1:50;
then A6: X' '||' Y by A1, A2, A3, AFF_4:42, AFF_4:56;
X' is being_line by A3, AFF_1:50;
hence a on A by A1, A4, A5, A6, Th29; :: thesis: verum