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