:: deftheorem defines are_collinear RLTOPSP1:def 16 :
for V being RealLinearSpace
for x1, x2, x3 being Point of V holds
( x1,x2,x3 are_collinear iff ex L being line of V st
( x1 in L & x2 in L & x3 in L ) );