let AS be AffinSpace; :: thesis: for a, b being Element of AS
for A being being_line Subset of AS 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 being_line Subset of AS 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 ) )
A1: for A being Subset of AS st a,b // A holds
ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d ) by Th27;
let A be being_line Subset of AS; :: 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
A2: c <> d and
A3: c in A and
A4: d in A and
A5: a,b // c,d ;
A = Line (c,d) by A2, A3, A4, Lm6;
hence a,b // A by A2, A5; :: 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