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) by Def3;
A3: b in A by A2, Th26;
a in A by A2, Th26;
hence ex a, b being Element of AS st
( a in A & b in A & a <> b ) by A1, A3; :: thesis: verum