let AS be AffinSpace; :: thesis: for X being Subset of
for p being POINT of
for A being LINE of st A = [X,1] & X is being_line & p on A & p is not Element of holds
p = LDir X
let X be Subset of ; :: thesis: for p being POINT of
for A being LINE of st A = [X,1] & X is being_line & p on A & p is not Element of holds
p = LDir X
let p be POINT of ; :: thesis: for A being LINE of st A = [X,1] & X is being_line & p on A & p is not Element of holds
p = LDir X
let A be LINE of ; :: thesis: ( A = [X,1] & X is being_line & p on A & p is not Element of implies p = LDir X )
assume that
A1: A = [X,1] and
A2: X is being_line and
A3: p on A and
A4: p is not Element of ; :: thesis: p = LDir X
consider Xp being Subset of such that
A5: p = LDir Xp and
A6: Xp is being_line by A4, Th20;
Xp '||' X by A1, A2, A3, A5, A6, Th28;
hence p = LDir X by A2, A5, A6, Th12; :: thesis: verum