let AS be AffinSpace; for X being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st X is being_line & a = LDir X & A = [X,1] holds
a on A
let X be Subset of AS; for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st X is being_line & a = LDir X & A = [X,1] holds
a on A
let a be POINT of (IncProjSp_of AS); for A being LINE of (IncProjSp_of AS) st X is being_line & a = LDir X & A = [X,1] holds
a on A
let A be LINE of (IncProjSp_of AS); ( 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]
; a on A
X // X
by A1, AFF_1:41;
then
X '||' X
by A1, AFF_4:40;
hence
a on A
by A1, A2, A3, Th28; verum