let AS be AffinSpace; :: thesis: for A being Subset of AS st A is being_line holds
ex q being Element of AS st not q in A
let A be Subset of AS; :: thesis: ( A is being_line implies ex q being Element of AS st not q in A )
assume A1: A is being_line ; :: thesis: not for q being Element of AS holds q in A
then consider a, b being Element of AS such that
A2: ( a in A & b in A ) and
A3: a <> b by AFF_1:19;
consider q being Element of AS such that
A4: not LIN a,b,q by A3, AFF_1:13;
not q in A by A1, A2, A4, AFF_1:21;
hence not for q being Element of AS holds q in A ; :: thesis: verum