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