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

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