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