let CLSP be CollSp; :: thesis: for a, b, r being Point of CLSP holds
( a,b,r is_collinear iff r in Line a,b )
let a, b, r be Point of CLSP; :: thesis: ( a,b,r is_collinear iff r in Line a,b )
thus ( a,b,r is_collinear implies r in Line a,b ) ; :: thesis: ( r in Line a,b implies a,b,r is_collinear )
thus ( r in Line a,b implies a,b,r is_collinear ) :: thesis: verum

proof

assume r in Line a,b ; :: thesis: a,b,r is_collinear
then ex p being Point of CLSP st
( r = p & a,b,p is_collinear ) ;
hence a,b,r is_collinear ; :: thesis: verum

end;