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