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

ex a, b being Element of AS st

( a in A & b in A & a <> b )

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

( a in A & b in A & a <> b ) )

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

( a in A & b in A & a <> b )

then consider a, b being Element of AS such that

A1: a <> b and

A2: A = Line (a,b) ;

A3: b in A by A2, Th14;

a in A by A2, Th14;

hence ex a, b being Element of AS st

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

ex a, b being Element of AS st

( a in A & b in A & a <> b )

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

( a in A & b in A & a <> b ) )

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

( a in A & b in A & a <> b )

then consider a, b being Element of AS such that

A1: a <> b and

A2: A = Line (a,b) ;

A3: b in A by A2, Th14;

a in A by A2, Th14;

hence ex a, b being Element of AS st

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