let AS be AffinSpace; :: thesis: for a being Element of AS
for A being being_line Subset of AS holds a,a // A
let a be Element of AS; :: thesis: for A being being_line Subset of AS holds a,a // A
let A be being_line Subset of AS; :: thesis: a,a // A
consider p, q being Element of AS such that
A1: p <> q and
A2: A = Line (p,q) by Def3;
a,a // p,q by Th12;
hence a,a // A by A1, A2, Def4; :: thesis: verum