fof(th_5c1_03,axiom,(![A,B,C]:((point(A)&point(B)&point(C)&ncol(A,B,C)&A!=B)=>(B!=C&C!=A)))).
