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