let AS be AffinSpace; :: thesis: for X being Subset of AS
for p, a 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 & a on A & a <> p & p is not Element of the carrier of AS holds
a is Element of AS
let X be Subset of AS; :: thesis: for p, a 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 & a on A & a <> p & p is not Element of the carrier of AS holds
a is Element of AS
let p, a 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 & a on A & a <> p & p is not Element of the carrier of AS holds
a is Element of AS
let A be LINE of (IncProjSp_of AS); :: thesis: ( A = [X,1] & X is being_line & p on A & a on A & a <> p & p is not Element of the carrier of AS implies a is Element of AS )
assume that
A1: ( A = [X,1] & X is being_line ) and
A2: ( p on A & a on A & a <> p ) and
A3: p is not Element of AS ; :: thesis: a is Element of AS
assume a is not Element of AS ; :: thesis: contradiction
then ( a = LDir X & p = LDir X ) by A1, A2, A3, Th34;
hence contradiction by A2; :: thesis: verum