let AS be AffinSpace; :: thesis: for c, a, b, 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 c, a, b, 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;
A4: ( d in Line a,b implies a,b // c,d )

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, Th19; :: thesis: verum

end;

( a,b // c,d implies d in Line a,b )

proof

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

end;

hence ( d in Line a,b iff a,b // c,d ) by A4; :: thesis: verum