let AS be AffinSpace; :: thesis: for X being Subset of AS
for p being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st A = [X,1] & X is being_line & p on A & p is not Element of AS holds
p = LDir X
let X be Subset of AS; :: thesis: for p being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st A = [X,1] & X is being_line & p on A & p is not Element of AS holds
p = LDir X
let p be POINT of (IncProjSp_of AS); :: thesis: for A being LINE of (IncProjSp_of AS) st A = [X,1] & X is being_line & p on A & p is not Element of AS holds
p = LDir X
let A be LINE of (IncProjSp_of AS); :: thesis: ( A = [X,1] & X is being_line & p on A & p is not Element of AS 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 AS ; :: thesis: p = LDir X
consider Xp being Subset of AS 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