let AS be AffinSpace; :: thesis: for X being Subset of
for a being POINT of
for A being LINE of st X is being_line & a = LDir X & A = [X,1] holds
a on A
let X be Subset of ; :: thesis: for a being POINT of
for A being LINE of st X is being_line & a = LDir X & A = [X,1] holds
a on A
let a be POINT of ; :: thesis: for A being LINE of st X is being_line & a = LDir X & A = [X,1] holds
a on A
let A be LINE of ; :: thesis: ( X is being_line & a = LDir X & A = [X,1] implies a on A )
assume that
A1: X is being_line and
A2: a = LDir X and
A3: A = [X,1] ; :: thesis: a on A
X // X by A1, AFF_1:55;
then X '||' X by A1, AFF_4:40;
hence a on A by A1, A2, A3, Th28; :: thesis: verum