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