let AS be AffinSpace; :: thesis: 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; :: thesis: 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); :: thesis: 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); :: 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:41;
then X '||' X by A1, AFF_4:40;
hence a on A by A1, A2, A3, Th28; :: thesis: verum