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

proof

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

end;