let AS be AffinSpace; :: thesis: for a, b being Element of AS
for A being Subset of AS st A is being_line holds
( a,b // A iff ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d ) )
let a, b be Element of AS; :: thesis: for A being Subset of AS st A is being_line holds
( a,b // A iff ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d ) )
let A be Subset of AS; :: thesis: ( A is being_line implies ( a,b // A iff ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d ) ) )
A1: ( a,b // A implies ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d ) )

proof

assume a,b // A ; :: thesis: ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d )
then consider c, d being Element of AS such that
A2: c <> d and
A3: A = Line c,d and
A4: a,b // c,d by Def4;
A5: d in A by A3, Th26;
c in A by A3, Th26;
hence ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d ) by A2, A4, A5; :: thesis: verum

end;

assume A6: A is being_line ; :: thesis: ( a,b // A iff ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d ) )
( ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d ) implies a,b // A )

proof

assume ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d ) ; :: thesis: a,b // A
then consider c, d being Element of AS such that
A7: c <> d and
A8: c in A and
A9: d in A and
A10: a,b // c,d ;
A = Line c,d by A6, A7, A8, A9, Lm6;
hence a,b // A by A7, A10, Def4; :: thesis: verum

end;

hence ( a,b // A iff ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d ) ) by A1; :: thesis: verum