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

end;

( 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
A4: ( c <> d & c in A & d in A & a,b // c,d ) ;
A = Line c,d by A1, A4, Lm6;
hence a,b // A by A4, 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 A2; :: thesis: verum