let CLSP be CollSp; 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; ( a,b,r are_collinear iff r in Line (a,b) )
thus
( a,b,r are_collinear implies r in Line (a,b) )
; ( r in Line (a,b) implies a,b,r are_collinear )
thus
( r in Line (a,b) implies a,b,r are_collinear )
verum