let AS be AffinSpace; :: thesis: for a, b, c, d being Element of AS st c in Line (a,b) & a <> b holds
( d in Line (a,b) iff a,b // c,d )
let a, b, c, d be Element of AS; :: thesis: ( c in Line (a,b) & a <> b implies ( d in Line (a,b) iff a,b // c,d ) )
assume that
A1: c in Line (a,b) and
A2: a <> b ; :: thesis: ( d in Line (a,b) iff a,b // c,d )
A3: LIN a,b,c by A1, Def2;
thus ( d in Line (a,b) implies a,b // c,d ) :: thesis: ( a,b // c,d implies d in Line (a,b) )

proof

assume d in Line (a,b) ; :: thesis: a,b // c,d
then LIN a,b,d by Def2;
hence a,b // c,d by A3, Th9; :: thesis: verum

end;

assume a,b // c,d ; :: thesis: d in Line (a,b)
then LIN a,b,d by A2, A3, Th8;
hence d in Line (a,b) by Def2; :: thesis: verum