let AS be AffinSpace; :: thesis: for a being Element of AS

for A being Subset of AS st A is being_line holds

ex b being Element of AS st

( a <> b & b in A )

let a be Element of AS; :: thesis: for A being Subset of AS st A is being_line holds

ex b being Element of AS st

( a <> b & b in A )

let A be Subset of AS; :: thesis: ( A is being_line implies ex b being Element of AS st

( a <> b & b in A ) )

assume A is being_line ; :: thesis: ex b being Element of AS st

( a <> b & b in A )

then consider p, q being Element of AS such that

A1: p in A and

A2: q in A and

A3: p <> q by Th18;

( a = p implies ( a <> q & q in A ) ) by A2, A3;

hence ex b being Element of AS st

( a <> b & b in A ) by A1; :: thesis: verum

for A being Subset of AS st A is being_line holds

ex b being Element of AS st

( a <> b & b in A )

let a be Element of AS; :: thesis: for A being Subset of AS st A is being_line holds

ex b being Element of AS st

( a <> b & b in A )

let A be Subset of AS; :: thesis: ( A is being_line implies ex b being Element of AS st

( a <> b & b in A ) )

assume A is being_line ; :: thesis: ex b being Element of AS st

( a <> b & b in A )

then consider p, q being Element of AS such that

A1: p in A and

A2: q in A and

A3: p <> q by Th18;

( a = p implies ( a <> q & q in A ) ) by A2, A3;

hence ex b being Element of AS st

( a <> b & b in A ) by A1; :: thesis: verum