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