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 Th2;

hence a,a // A by A1, A2; :: thesis: verum

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 Th2;

hence a,a // A by A1, A2; :: thesis: verum